fix mode signature

LPCIC · Dec 16, 2024 · ea94bb1 · ea94bb1
1 parent 069018b
commit ea94bb1
Show file tree

Hide file tree

Showing 8 changed files with 9 additions and 15 deletions.
diff --git a/apps/derive/elpi/eqb.elpi b/apps/derive/elpi/eqb.elpi
@@ -2,7 +2,7 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-type feqb.trm->term trm -> term -> prop.
+pred feqb.trm->term i:trm, o:term.
 
 macro @pi-trm N T F :-
   pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.

diff --git a/apps/derive/elpi/eqbOK.elpi b/apps/derive/elpi/eqbOK.elpi
@@ -3,7 +3,7 @@
 /* ------------------------------------------------------------------------- */
 
 
-type feqb.trm->term trm -> term -> prop.
+pred feqb.trm->term i:trm, o:term.
 
 macro @pi-trm N T F :-
   pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.

diff --git a/apps/derive/elpi/eqbcorrect.elpi b/apps/derive/elpi/eqbcorrect.elpi
@@ -2,7 +2,7 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-type feqb.trm->term trm -> term -> prop.
+pred feqb.trm->term i:trm, o:term.
 
 macro @pi-trm N T F :-
   pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.

diff --git a/apps/derive/theories/derive/eq.v b/apps/derive/theories/derive/eq.v
@@ -29,7 +29,7 @@ type eq-for inductive -> constant -> prop.
 #[superglobal] Elpi Accumulate derive.eq.db File derive.lib.
 #[superglobal] Elpi Accumulate derive.eq.db lp:{{
 
-type whd1 term -> term -> prop.
+pred whd1 i:term, o:term.
 
 :name "eq-db:fail"
 eq-db A B F :-

diff --git a/apps/derive/theories/derive/eqb.v b/apps/derive/theories/derive/eqb.v
@@ -15,7 +15,7 @@ Require Import eqType_ast tag fields.
 Register eqb_body as elpi.derive.eqb_body.
 
 Elpi Db derive.eqb.db lp:{{
-  type whd1 term -> term -> prop.
+  pred whd1 i:term, o:term.
 
   pred eqb-done o:gref.
 

diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
@@ -130,7 +130,7 @@ namespace tc {
       }
     }
 
-    pred eta i:term, o:term.
+    pred eta i:term, i:term.
     eta A B :- eta.eta A B.
 
     pred solve-eta.

diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
@@ -18,23 +18,14 @@ Set Warnings "+elpi".
 
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
-
 Elpi Accumulate Db tc_options.db.
-
 Elpi Accumulate File tc_aux.
-
 Elpi Accumulate File ho_precompile.
-
 Elpi Accumulate File unif.
-
 Elpi Accumulate File ho_link.
-
 Elpi Accumulate File ho_compile.
-
 Elpi Accumulate File compiler1.
-
 Elpi Accumulate File modes.
-
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
@@ -99,6 +99,9 @@ Elpi Db tc.db lp:{{
     pred dummy.
 
     pred ho-link o:term, i:term, o:A.
+    pred link.eta i:term, i:term.
+    pred link.llam i:term, i:term.
+
   }
 }}.
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.