Variable rename

LPCIC · Nov 7, 2023 · 13c3290 · 13c3290
1 parent d2c2955
commit 13c3290
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi
@@ -98,9 +98,9 @@ compile-aux (prod N T F) I RevPremises ListVar [] IsPositive IsHead Clause ff :-
     compile-aux (F p) I L [p | ListVar] [] IsPositive IsHead (C p) _.
 compile-aux Ty I RevPremises ListVar [] _ IsHead Clause tt :- 
   not (is-option-active {oTC-use-pattern-fragment-compiler}), !,
-  std.rev RevPremises RevRHS,
+  std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,
-  make-tc IsHead Ty AppInst RevRHS Clause.
+  make-tc IsHead Ty AppInst Premises Clause.
 compile-aux Ty I RevPremises ListVar [] IsPositive IsHead Clause tt :- !,
   std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,