[TC] avoid a backtrack

LPCIC · Aug 20, 2024 · f348d07 · f348d07
1 parent 268a8b3
commit f348d07
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
@@ -198,7 +198,7 @@ namespace tc {
       cs (uvar _ as V) (app [HD | _] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
-          (coq.unify-eq V T ok).
+          (coq.unify-eq V T ok), !.
       cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
 
       pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.