fix a bunch of warnings

apps/derive/elpi/derive.elpi

@@ -19,7 +19,7 @@ dep X Y :- dep1 X Z, dep Z Y.
 
 func selected string ->.
 selected Name :- get-option "only" Map, !,
-  Map => (get-option Name _; (get-option X _, dep X Name)), !.
+  Map =!=> (get-option Name _; (get-option X _, dep X Name)), !.
 selected _.
 
 func validate-only gref, list derive ->.
@@ -44,13 +44,13 @@ chain T [derive Name F _|FS] CL :- get-option "only" _, !, % request this one
   if-verbose (coq.say "Derivation" Name "on" T),
   (@dropunivs! ==> std.time (F C) Time),
   if-verbose (coq.say "Derivation" Name "on" T "took" Time),
-  (C ==> chain T FS CS),
+  (C =!=> chain T FS CS),
   std.append C CS CL.
 chain T [derive Name F _|FS] CL :- % all are selected, we can fail
   if-verbose (coq.say "Derivation" Name "on" T),
   ((pi x\ stop x :- !, fail) ==> @dropunivs! ==> std.time (F C) Time), !,
   if-verbose (coq.say "Derivation" Name "on" T "took" Time),
-  (C ==> chain T FS CS),
+  (C =!=> chain T FS CS),
   std.append C CS CL.
 chain T [derive F _ _|FS] CL :-
   if-verbose (coq.say "Derivation" F "on" T "failed, continuing"),
@@ -102,15 +102,15 @@ main-derive GR InModule CL :- get-option "recursive" tt, !,
   coq.gref.set.elements AllDeps AllDepsL,
   std.filter AllDepsL indt-or-const Deps,
   main.aux InModule Deps [] CL1,
-  (CL1 ==> main1 GR InModule CL2),
+  (CL1 =!=> main1 GR InModule CL2),
   std.append CL1 CL2 CL.
 main-derive GR InModule CL :- main1 GR InModule CL.
 
 :index (_ 1)
 func main.aux bool, list gref, list prop -> list prop.
 main.aux _ [] X X.
 main.aux InModule [GR|GRS] Acc CL :-
-  ((pi X\get-option "only" X :- !, fail) ==> Acc ==> main-derive GR InModule CL1),
+  ((pi X\get-option "only" X :- !, fail) ==> Acc =!=> main-derive GR InModule CL1),
   main.aux InModule GRS {std.append CL1 Acc} CL.
 
 func validate-recursive prop -> derive.

apps/derive/elpi/derive_synterp.elpi

@@ -10,7 +10,7 @@ dep X Y :- dep1 X Z, dep Z Y.
 
 func selected string ->.
 selected Name :- get-option "only" Map, !,
-  Map ==> (get-option Name _; (get-option X _, dep X Name)), !.
+  Map =!=> (get-option Name _; (get-option X _, dep X Name)), !.
 selected _.
 
 :index (_ 1)

apps/derive/elpi/eq.elpi

@@ -53,18 +53,18 @@ bo-idx C Ity1 (prod _ Src1 Tgt1) Ity2 (prod _ Src2 Tgt2) N M Rty R :- !,
   Rty = (prod I1 Src1 i\ prod I2 Src2 j\ Rtyrec i j),
   quantify-eq-db-idx C Crec,
   pi x y\
-   decl x `i` Src1 =>
-   decl y `j` Src2 =>
+   decl x `i` Src1 ==>
+   decl y `j` Src2 ==>
    bo-idx Crec {coq.mk-app Ity1 [x]} (Tgt1 x) {coq.mk-app Ity2 [y]} (Tgt2 y) 
      {calc (N + 2)} M (Rtyrec x y) (Rrec x y).
 
 bo-idx C Ity1 (sort _) Ity2 (sort _) N N Rty R :- !,
   Rty = {{ lp:Ity1 -> lp:Ity2 -> bool }},
   R = {{ fun (x1 : lp:Ity1) (x2 : lp:Ity2) => lp:(Bo x1 x2) }},
   pi x1 x2\
-   decl x1 `a` Ity1 =>
-   decl x2 `b` Ity2 =>
-   C =>
+   decl x1 `a` Ity1 ==>
+   decl x2 `b` Ity2 ==>
+   C =!=>
      bo-matrix x1 Ity1 x2 Ity2 (Bo x1 x2).
 
 bo-idx C Ity1 X Ity2 Y N M Rty R :- whd1 X X1, whd1 Y Y1, !,

apps/derive/elpi/eqbcorrect.elpi

@@ -135,7 +135,7 @@ run-solver G Name :-
 func coq.sealed-goal->string sealed-goal -> string.
 coq.sealed-goal->string (nabla G) R :- pi x\  coq.sealed-goal->string (G x) R.
 coq.sealed-goal->string (seal (goal Ctx _ Ty _ _)) R :-
-  Ctx => (std.map {std.rev Ctx} coq.ctx->string L, coq.term->string Ty G, R is "Lemma foo " ^ {std.string.concat "\n" L} ^ "\n :\n" ^ G ^ ".").
+  Ctx =!=> (std.map {std.rev Ctx} coq.ctx->string L, coq.term->string Ty G, R is "Lemma foo " ^ {std.string.concat "\n" L} ^ "\n :\n" ^ G ^ ".").
 
 func coq.ctx->string prop -> string.
 coq.ctx->string (decl X _ Ty) R :- R is "(" ^ {coq.term->string X} ^ " : " ^ {coq.term->string Ty} ^ ")".

apps/derive/elpi/fields.elpi

@@ -26,20 +26,20 @@ main I Prefix AllCL :- std.do! [
 
   box (global (indt I)) KS FI CLB,
 
-  (CLB ==> fields_t.main FI (global (indt I)) Body_t),
+  (CLB =!=> fields_t.main FI (global (indt I)) Body_t),
   std.assert-ok! (coq.typecheck Body_t Ty_t) "derive.fields generates illtyped fields_t",
   Name_t is Prefix ^ "fields_t",
   coq.ensure-fresh-global-id Name_t FName_t,
   coq.env.add-const FName_t Body_t Ty_t ff Fields_t, 
 
-  (CLB ==> fields.main FI (global (indt I)) (global (const Fields_t)) (global (const Tag)) BodySkel),
+  (CLB =!=> fields.main FI (global (indt I)) (global (const Fields_t)) (global (const Tag)) BodySkel),
   % we elaborate only for primitive records...
   std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "derive.fields generates illtyped fields",
   Name is Prefix ^ "fields",
   coq.ensure-fresh-global-id Name FName,
   coq.env.add-const FName Body Ty ff Fields, 
 
-  (CLB ==> construct.main FI (global (indt I)) Fields_t Body_c),
+  (CLB =!=> construct.main FI (global (indt I)) Fields_t Body_c),
   std.assert-ok! (coq.typecheck Body_c Ty_c) "derive.fields generates illtyped construct",
   Name_c is Prefix ^ "construct",
   coq.ensure-fresh-global-id Name_c FName_c,
@@ -125,7 +125,7 @@ box.declare [K|Ks] [real-box I|Bs] [C|Cs] :-
   coq.env.add-indt D IB,
   coq.env.indt IB _ _ _ _ [KB] _,
   C = box-for K IB KB,
-  (C ==> box.declare Ks Bs Cs).
+  (C =!=> box.declare Ks Bs Cs).
 box.declare [K|Ks] [same-box K1|Bs] [box-for K IB KB|Cs] :-
   box-for K1 IB KB,
   box.declare Ks Bs Cs.
@@ -159,7 +159,7 @@ box.aux2 I Ind X [eqb.constructor K Args|MoreKs] [real-box (record ID1 S ID2 Fie
   ID1 is "box_" ^ {coq.gref->id (indt Ind)} ^ "_" ^ {coq.gref->id (indc K)},
   ID2 is "Box_" ^ {coq.gref->id (indt Ind)} ^ "_" ^ {coq.gref->id (indc K)},
   ((feqb.trm->term X I :- !) ==> box.box-argument ID2 0 Args Fields),
-  args-of K Args ==> box.aux2 I Ind X MoreKs MoreBoxes.
+  args-of K Args =!=> box.aux2 I Ind X MoreKs MoreBoxes.
 
 :index(_ _ 1)
 func box.box-argument string, int, eqb.arguments -> record-decl.

apps/derive/elpi/idx2inv.elpi

@@ -17,7 +17,7 @@ params (inductive _ _ Arity _) T Ti (fix `rec` N FixTy FixBo) :- coq.safe-dest-a
   compute-fix-ty Ty T Ti N FixTy,
   compute-fix-clause Ty T Ti N Prove,
   compute-fix-clause Ty T Ti {calc (N + 1)} Prove1,
-  @pi-decl `rec` Ty f\ Prove f => Prove1 f => compute-fix-bo Ty T Ti (FixBo f).
+  @pi-decl `rec` Ty f\ Prove f =!=> Prove1 f =!=> compute-fix-bo Ty T Ti (FixBo f).
 params (inductive _ _ Arity _) T Ti Bo :-
   coq.arity->term Arity Ty,
   compute-fix-bo Ty T Ti Bo.

apps/derive/elpi/induction.elpi

@@ -46,7 +46,7 @@ branches (sort _) Ity Args IH Rno Rno Fty (fun `x` ItyArgs Bo) :- do! [
   copy Ity P,
   mk-paramX.prove-clause Args Ity P IH C,
   @pi-decl `x` ItyArgs x\
-    C =>
+    C =!=>
     coq.build-match x ItyArgs oty branch (Bo x)
 ].
 
@@ -131,7 +131,7 @@ main GR Prefix [Clause] :- do! [
   assert! (Ind = tt) "derive.induction: Coinductive types are not supported",
 
   % we build the induction principle
-  Informative => params Lno TR {std.map K (k\r\ r = global (indc k))} KT Arity R,
+  Informative =!=> params Lno TR {std.map K (k\r\ r = global (indc k))} KT Arity R,
   % coq.say {coq.term->string R},
   std.assert-ok! (coq.typecheck R RT) "derive.induction generates illtyped term",
 

apps/derive/elpi/map.elpi

@@ -100,7 +100,7 @@ bo-params N Lno Ity1 Ity2 (prod A Sty1 Rty1) (prod _ Sty2 Rty2) Ps R :-
   pi a b f\ sigma Ity1A Ity2A \
     coq.mk-app Ity1 [a] Ity1A,
     coq.mk-app Ity2 [b] Ity2A,
-    Clause a b f =>
+    Clause a b f =!=>
     decl a A1 Sty1 =>
     decl b A2 Sty2 =>
     decl f Af (FAB a b) =>

apps/derive/elpi/param1_congr.elpi

@@ -58,7 +58,7 @@ main _ (indt GR) Prefix Clauses2 :-
   forall Clauses2
     (x\ coq.elpi.accumulate _ "derive.param1.congr.db" (clause _ _ x)).
 
-main _ (const IsGR) Prefix [param1-congr-done (const IsGR)].
+main _ (const IsGR) _ [param1-congr-done (const IsGR)].
 
 }
 

apps/derive/elpi/param1_functor.elpi

@@ -100,7 +100,7 @@ bo-params Lno Lno Ity1 Ity2 A1 _ Ps (fix `f` Recno Fty Bo) :- !,
   @pi-decl `rec` Fty f\
       mk-rec-clause A1 Ity1 Ity2 f (C f),
       mk-rec-clause-app A1 Ity1 Ity2 f (D f),
-      (D f) => (C f) => bo-idx A1 Ity1 Ity2 0 Recno Ps (Bo f) Fty.
+      (D f) =!=> (C f) =!=> bo-idx A1 Ity1 Ity2 0 Recno Ps (Bo f) Fty.
 
 bo-params N Lno Ity1 Ity2 {{ forall (a : lp:T1) (p : a -> Type), lp:(Rty1 a p) }}
                           {{ forall (a : _) (p : a -> Type), lp:(Rty2 a p) }}
@@ -111,7 +111,7 @@ bo-params N Lno Ity1 Ity2 {{ forall (a : lp:T1) (p : a -> Type), lp:(Rty1 a p) }
   pi a pa pb f\ sigma Ity1A Ity2A \
     coq.mk-app Ity1 [a,pa] Ity1A,
     coq.mk-app Ity2 [a,pb] Ity2A,
-    Clause pa pb f =>
+    Clause pa pb f =!=>
     decl a `a` {{ Type }} =>
     decl pa `pa` {{ lp:a -> Type }} =>
     decl pb `pb` {{ lp:a -> Type }} =>

apps/derive/elpi/param1_inhab.elpi

@@ -52,7 +52,7 @@ body-params 0 IsT (prod _ T _\ sort _) K KT R :- coq.safe-dest-app T (global (in
   R = {{ fix IH (x : lp:T) {struct x} : lp:(RT x) := lp:(Bo IH x) }},
   coq.env.indt GR _ _ _ _ KX _,
   map2 KX {zip K KT} (a\b\r\ r = (global (indc a)) `-> b) K2KR,
-  K2KR => % K `-> (pr isK isKtype)
+  K2KR =!=> % K `-> (pr isK isKtype)
     @pi-decl `IH` (prod `x` T x\ RT x) f\
     @pi-decl `x` T x\
     param1-inhab-db IsT f =>
@@ -66,7 +66,7 @@ body-params 0 IsT (prod _ T _\ sort _) K KT R :- !,
   coq.safe-dest-app T (global (indt GR)) _,
   coq.env.indt GR _ _ _ _ KX _,
   map2 KX {zip K KT} (a\b\r\ r = (global (indc a)) `-> b) K2KR,
-  K2KR => % K `-> (pr isK isKtype)
+  K2KR =!=> % K `-> (pr isK isKtype)
   @pi-decl `x` T x\
     coq.build-match x T (oty RT) body (Bo x).
 

apps/derive/elpi/param1_trivial.elpi

@@ -126,7 +126,7 @@ main _ (indt GR) Suffix [Clause,param1-trivial-done (indt GR)] :- do! [
   coq.elpi.accumulate _ "derive.param1.trivial.db" (clause _ _ (param1-trivial-done (indt GR))),
 ].
 main (const GR) (const IsGR) Suffix [Clause,param1-trivial-done (const IsGR)] :- do! [
-  coq.env.const GR (some T) _,
+  coq.env.const GR (some _) _,
   coq.env.const IsGR (some IsT) _,
   Name is {coq.gref->id (const IsGR)} ^ Suffix,
 

apps/derive/elpi/paramX_lib.elpi

@@ -27,7 +27,7 @@ mk-trivial-match -1 P RArgs F Match :- std.do! [
 func mk-trivial-match.rty list term, term,  term, list term, list term -> term.
 mk-trivial-match.rty Args P _ Vars _ R :- std.do! [
   std.map2 Args Vars (x\y\r\ r = copy x y) Subst,
-  Subst => copy P R,
+  Subst =!=> copy P R,
 ].
 
 func mk-trivial-match.branch int, list term, list term, term,  term, term, list term, list term -> term.
@@ -37,7 +37,7 @@ mk-trivial-match.branch Lno Args OtherArgs F K KTy Vars _ R1 :- std.do! [
   std.drop Lno KTyArgs IdxVals,
   std.map2 Args IdxVals (x\y\r\ r = copy x y) Subst,
   (R = let `K` KTy KArgs x\ {coq.mk-app F {std.append OtherArgs [x]}}),
-  Subst => copy R R1,
+  Subst =!=> copy R R1,
 ].
 
 

apps/derive/elpi/projK.elpi

@@ -79,7 +79,7 @@ body-default (prod N T F) J OJ IT Args K (fun N T B) :- !,
     if (J = OJ)
       (Def = [default-output J Mask Args x T])
       (Def = []),
-    Def ==> body-default (F x) J1 OJ IT {append Args [pr x T]} K (B x).
+    Def =!=> body-default (F x) J1 OJ IT {append Args [pr x T]} K (B x).
 
 body-default X J OJ IT Args K F :- whd1 X X1, !,
   body-default X1 J OJ IT Args K F.

apps/derive/theories/derive.v

@@ -75,7 +75,7 @@ Elpi Accumulate lp:{{
       att "module" string,
       att "no_alias" bool,
     ] Opts, !,
-    Opts => P.
+    Opts =!=> P.
 
   pred get_name i:indt-decl, o:string.
   get_name (parameter _ _ _ F) N :- pi p\ get_name (F p) N.

apps/derive/theories/derive/param1_trivial.v

@@ -93,7 +93,7 @@ Elpi Accumulate lp:{{
     realiR T {coq.env.global IsGR},
     coq.env.global GR T,
     derive.param1.inhab.main GR IsGR "_inhab" CL,
-    CL => derive.param1.trivial.main GR IsGR "_trivial" _.
+    CL =!=> derive.param1.trivial.main GR IsGR "_trivial" _.
   main _ :- usage.
 
   usage :-

apps/derive/theories/dune

@@ -1,6 +1,7 @@
 (coq.theory
  (name elpi.apps.derive)
  (package rocq-elpi)
+ (flags -w +elpi.deprecated -w +elpi.implication-precedence -w +elpi.flex-clause -w +elpi.typecheck)
  (theories elpi elpi.apps.derive.elpi))
 
 (include_subdirs qualified)

dune

@@ -1,4 +1,4 @@
 (env
  (dev
   (flags (:standard -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A))
-  (coq (flags -w +elpi.deprecated -w +elpi.implication-precedence -w -elpi.flex-clause -bt))))
+  (coq (flags -w +elpi.deprecated -w +elpi.implication-precedence -w +elpi.flex-clause -w +elpi.typecheck -bt))))

src/rocq_elpi_vernacular.ml

@@ -299,7 +299,7 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x)
     | `Db _ -> err ~loc:(of_coq_loc loc) Pp.(str "TODO")
     | `Program base ->
         let b =
-          try Elpi.API.BuiltIn.of_file id
+          try Elpi.API.BuiltIn.of_file ~file_name:id
           with Not_found -> err ~loc:(of_coq_loc loc) Pp.(str "Elpi plugin " ++ str id ++
             str " not found." ++ spc () ++ str "Did you have a Declare ML Module for the plugin?"++ spc () ++
             str "Does the plugin run Elpi.API.BuiltIn.declare ~file_name:\"" ++ str id ++ str "\"?") in