From ea94bb1663704a692d7a57058fded56636cea07f Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Mon, 16 Dec 2024 17:14:25 +0100
Subject: [PATCH] fix mode signature

---
 apps/derive/elpi/eqb.elpi         | 2 +-
 apps/derive/elpi/eqbOK.elpi       | 2 +-
 apps/derive/elpi/eqbcorrect.elpi  | 2 +-
 apps/derive/theories/derive/eq.v  | 2 +-
 apps/derive/theories/derive/eqb.v | 2 +-
 apps/tc/elpi/ho_link.elpi         | 2 +-
 apps/tc/theories/add_commands.v   | 9 ---------
 apps/tc/theories/db.v             | 3 +++
 8 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/apps/derive/elpi/eqb.elpi b/apps/derive/elpi/eqb.elpi
index a97671577..bd3997e9b 100644
--- 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
index a997d72e5..8b9d4c512 100644
--- 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
index 5b72c7a4b..46cf5cbd7 100644
--- 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
index 1dadda698..55ca01dec 100644
--- 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
index 83685e389..cdfe46db3 100644
--- 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
index 5a7afff00..fe4105019 100644
--- 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
index a8096e1e6..822436593 100644
--- 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
index 324b38eff..b8571dd2b 100644
--- 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.