From 663f89505834b90a85cfe0f725c0c1b5c8d98104 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 4 Aug 2020 20:53:01 +0100 Subject: [PATCH] Fix unification error A typo! But it causes some things to fail to unify, especially in proof search. --- src/Core/Unify.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index e044bbe2e..abe3f2460 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -764,7 +764,7 @@ mutual unifyHoleApp swap mode loc env mname mref margs margs' (NDCon nfc n t a args') = do defs <- get Ctxt mty <- lookupTyExact n (gamma defs) - unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NTCon nfc n t a) args' + unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NDCon nfc n t a) args' unifyHoleApp swap mode loc env mname mref margs margs' (NApp nfc (NLocal r idx p) args') = unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing (NApp nfc (NLocal r idx p)) args'