add tc.maybe-llam-tm in clean-term

LPCIC · May 6, 2024 · b055d23 · b055d23
1 parent 79a94e6
commit b055d23
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
@@ -108,6 +108,7 @@ namespace tc {
       clean-term A B :-
         (pi t s r\ copy (tc.maybe-eta-tm t s) r :- !, copy t r) =>
         (pi t s r\ copy (tc.maybe-beta-tm t s) r :- !, copy t r) =>
+        (pi t s r\ copy (tc.maybe-llam-tm t s) r :- !, copy t r) =>
           std.assert! (copy A B) "[TC] clean-term error".
 
       pred add-pi-problematic-terms

diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
@@ -41,7 +41,7 @@ namespace tc {
 
     pred progress-eta-left i:term, o:term.
     progress-eta-left A _ :- var A, !, fail.
-    progress-eta-left (fun _ _ A) (fun _ _ B) :- var B, !, A = B.
+    progress-eta-left (fun _ _ A) (fun _ _ A).
     progress-eta-left A A' :- (name A; is-coq-term A), !, eta-expand A A'.
 
     pred progress-eta-right i:term, o:term.