Revert "Revert "[TC] clean-term also for tc.canonical-projection""

This reverts commit 48c6cae.
LPCIC · Jul 10, 2024 · a3aaeb3 · a3aaeb3
1 parent 48c6cae
commit a3aaeb3
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
@@ -119,6 +119,7 @@ namespace tc {
       pred clean-term i:term, o:term.
       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.canonical-projection t s _) r :- !, copy t r, !) =>
         (pi t s r \ copy (tc.prod-range 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".