eradicate => warnings

apps/derive/elpi/derive.elpi

@@ -36,20 +36,20 @@ chain _ [] [].
 chain T [derive Name _ _|FS] CL :- not(selected Name), !,
   if-verbose (coq.say "Skipping derivation" Name "on" T "since the user did not select it"),
   chain T FS CL.
-chain T [derive Name _ AlreadyDone|FS] CL :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
+chain T [derive Name _ AlreadyDone|FS] CL :- ((pi x\ stop x :- !, fail) ==> AlreadyDone), !,
   if-verbose (coq.say "Skipping derivation" Name "on" T "since it has been already run"),
   chain T FS CL.
 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,
+  (@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, !,
+  ((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"),
@@ -105,14 +105,14 @@ 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.
 
 pred main.aux i:bool, i:list gref, i:list prop, o: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.
 
 pred validate-recursive i:prop, o:derive.
@@ -170,11 +170,11 @@ decl+main.post TypeName I DS CL :- std.do! [
 
   coq.indt-decl->implicits DS IndImpls KsImpls,
   if (coq.any-implicit? IndImpls)
-     (@global! => coq.arguments.set-implicit (indt I) [IndImpls])
+     (@global! ==> coq.arguments.set-implicit (indt I) [IndImpls])
      true,
   std.forall2 KsImpls KS (i\k\
     if (coq.any-implicit? i)
-       (@global! => coq.arguments.set-implicit (indc k) [i])
+       (@global! ==> coq.arguments.set-implicit (indc k) [i])
        true
     ),
   std.map-filter CL export? P,
@@ -183,6 +183,6 @@ decl+main.post TypeName I DS CL :- std.do! [
 
 pred short-alias i:id, i:term.
 short-alias _ _ :- get-option "no_alias" tt, !, true.
-short-alias ID T :- @global! => coq.notation.add-abbreviation ID 0 T ff _.
+short-alias ID T :- @global! ==> coq.notation.add-abbreviation ID 0 T ff _.
 
 }

apps/derive/elpi/derive_synterp.elpi

@@ -10,20 +10,20 @@ dep X Y :- dep1 X Z, dep Z Y.
 
 pred selected i: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 _.
 
 pred chain i:string, i:list derive.
 chain _ [].
 chain T [derive Name _ _|FS] :- not(selected Name), !,
   chain T FS.
-chain T [derive _ _ AlreadyDone|FS] :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
+chain T [derive _ _ AlreadyDone|FS] :- ((pi x\ stop x :- !, fail) ==> AlreadyDone), !,
   chain T FS.
 chain T [derive _ F _|FS] :- get-option "only" _, !, % request this one
   F _,
   chain T FS.
 chain T [derive _ F _|FS] :- % all are selected, we can fail
-  (pi x\ stop x :- !, fail) => F _, !,
+  ((pi x\ stop x :- !, fail) ==> F _), !,
   chain T FS.
 chain T [derive _ _ _|FS] :-
   chain T FS.

apps/derive/elpi/eqb.elpi

@@ -204,9 +204,9 @@ fields.aux (dependent TYX FX) (dependent TYY FY) [X|XS] [Y|YS] {{ lib:elpi.andb
   feqb.trm->term TYX TX,
   feqb.trm->term TYY TY,
   mk-eqb-for TX TY EQB,
-  @pi-decl `p` TX n\ pi a\ (feqb.trm->term a n :- !) =>
-  @pi-decl `p` TY m\ pi b\ (feqb.trm->term b m :- !) =>
-    fields.aux (FX a) (FY b) XS YS (R n m),
+  (@pi-decl `p` TX n\ pi a\ (feqb.trm->term a n :- !) ==>
+   @pi-decl `p` TY m\ pi b\ (feqb.trm->term b m :- !) ==>
+    fields.aux (FX a) (FY b) XS YS (R n m)),
   R1 = R X Y.
 
 fields.aux (regular TYX FX) (regular TYY FY)  [X|XS] [Y|YS] {{ lib:elpi.andb (lp:EQB lp:X lp:Y) lp:R }} :- 

apps/derive/elpi/eqbcorrect.elpi

@@ -29,8 +29,8 @@ main (indt I) Prefix CLs :- std.do! [
 
   /* Correctness */
 
-  config {{ @eqb_correct }} {{ @eqb_correct_on }} {{ @eqb_body_correct }} "eqb_correct_on__solver" correct-lemma-for =>
-    common FI [] Indu R,
+  (config {{ @eqb_correct }} {{ @eqb_correct_on }} {{ @eqb_body_correct }} "eqb_correct_on__solver" correct-lemma-for =>
+    common FI [] Indu R),
 
   %std.assert! (ground_term R) "ww",
   std.assert-ok! (coq.typecheck R Ty) "derive.eqbcorrect: common/correct generates ill typed term", 
@@ -40,8 +40,8 @@ main (indt I) Prefix CLs :- std.do! [
 
   if (has-params? FI) (
 
-    config {{ @eqb_correct }} {{ @eqb_correct_on }} {{ @eqb_body_correct }} "eqb_correct_on__solver" correct-lemma-for =>
-      common-aux FI [] Indu Rx,
+    (config {{ @eqb_correct }} {{ @eqb_correct_on }} {{ @eqb_body_correct }} "eqb_correct_on__solver" correct-lemma-for =>
+      common-aux FI [] Indu Rx),
 
     std.assert-ok! (coq.typecheck Rx Tyx) "derive.eqbcorrect: common-aux/corect generates ill typed term", 
     Namex is Prefix ^ "eqb_correct_aux",
@@ -53,8 +53,8 @@ main (indt I) Prefix CLs :- std.do! [
 
   /* Reflexivity */
 
-  config {{ @eqb_reflexive }} {{ @eqb_refl_on }} {{ @eqb_body_refl }} "eqb_refl_on__solver" refl-lemma-for =>
-    common FI [] Indu Rr,
+  (config {{ @eqb_reflexive }} {{ @eqb_refl_on }} {{ @eqb_body_refl }} "eqb_refl_on__solver" refl-lemma-for =>
+    common FI [] Indu Rr),
 
   std.assert-ok! (coq.typecheck Rr Tyr) "derive.eqbcorrect: common/refl generates ill typed term", 
   Namer is Prefix ^ "eqb_refl",
@@ -63,8 +63,8 @@ main (indt I) Prefix CLs :- std.do! [
 
   if (has-params? FI) (
 
-    config {{ @eqb_reflexive }} {{ @eqb_refl_on }} {{ @eqb_body_refl }} "eqb_refl_on__solver" refl-lemma-for =>
-      common-aux FI [] Indu Rrx,
+    (config {{ @eqb_reflexive }} {{ @eqb_refl_on }} {{ @eqb_body_refl }} "eqb_refl_on__solver" refl-lemma-for =>
+      common-aux FI [] Indu Rrx),
 
     std.assert-ok! (coq.typecheck Rrx Tyrx) "derive.eqbcorrect: common-aux/refl generates ill typed term", 
     Namerx is Prefix ^ "eqb_refl_aux",
@@ -125,7 +125,7 @@ search-eqcorrect-apply (inductive _ _) [] C R C R.
 pred run-solver i:sealed-goal, i:string.
 run-solver G Name :-
   if (coq.ltac.open (coq.ltac.call Name []) G []) true
-     (@holes! => coq.sealed-goal->string G SG,
+     ((@holes! => coq.sealed-goal->string G SG),
       std.fatal-error {calc ( "solver " ^ Name ^ " fails on goal:\n" ^ SG )}).
 
 pred coq.sealed-goal->string i:sealed-goal, o:string.

apps/derive/elpi/fields.elpi

@@ -3,7 +3,7 @@
 /* ------------------------------------------------------------------------- */
 
 macro @pi-trm N T F :-
-  pi x xx\ decl x N T => (feqb.trm->term xx x :- !) => F xx x.
+  pi x xx\ decl x N T ==> (feqb.trm->term xx x :- !) ==> F xx x.
 
 namespace derive.fields {
 
@@ -13,7 +13,7 @@ pred self o:term.
 
 pred std.stop-do! i:list prop.
 std.stop-do! [].
-std.stop-do! [P|PS] :- coq.say P, (pi x\ stop x :- !, fail) => P, !, std.stop-do! PS.
+std.stop-do! [P|PS] :- coq.say P, ((pi x\ stop x :- !, fail) ==> P), !, std.stop-do! PS.
 std.stop-do! [P|_] :- coq.say "STOP" P.
 
 pred main i:inductive, i:string, o:list prop.
@@ -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,
@@ -124,7 +124,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.
@@ -156,8 +156,8 @@ box.aux2 I Ind X [constructor K Args|MoreKs] [real-box (record ID1 S ID2 Fields)
   if (coq.env.informative? Ind) (S = {{ Type }}) (S = {{ Prop }}),
   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.
+  ((feqb.trm->term X I :- !) ==> box.box-argument ID2 0 Args Fields),
+  args-of K Args ==> box.aux2 I Ind X MoreKs MoreBoxes.
 
 pred box.box-argument i:string, i:int, i:arguments, o:record-decl.
 box.box-argument _ _ (stop _) end-record.
@@ -167,7 +167,7 @@ box.box-argument S M (irrelevant T Args) (field [] N TY _\A) :- N is S ^ "_" ^ {
   feqb.trm->term T TY, box.box-argument S {calc (M + 1)} Args A.
 box.box-argument S M (dependent T Args) (field [] N TY A) :- N is S ^ "_" ^ {std.any->string M},
   feqb.trm->term T TY,
-  pi x y\ (feqb.trm->term x y :- !) => box.box-argument S {calc (M + 1)} (Args x) (A y).
+  pi x y\ (feqb.trm->term x y :- !) ==> box.box-argument S {calc (M + 1)} (Args x) (A y).
 
 pred distribute i:(A -> list box-spec), i:((A -> indt-decl) ->  indt-decl -> prop), o:list box-spec.
 distribute (_\ []) _ [].

apps/derive/elpi/induction.elpi

@@ -23,9 +23,9 @@ mk-paramX.prove-clause [_,_|Args] T P IH (pi x y\ C x y) :-
 pred branch i:term, i:term, i:list term, i:list term, o:term. 
 branch K _ V VT R :-
   induction-hyp-db K IH,
-  (pi H G P\ paramX.prove H G P :- param1-functor-db H G P) =>
-  (pi X\ paramX.cross X) =>
-    paramX.prove-args V VT Args,
+  ((pi H G P\ paramX.prove H G P :- param1-functor-db H G P) ==>
+   (pi X\ paramX.cross X) ==>
+    paramX.prove-args V VT Args),
   coq.mk-app IH Args R.
 
 pred oty i:term, i:list term, i:list term, o:term.

apps/derive/elpi/lens.elpi

@@ -68,7 +68,7 @@ declare-lens Prefix I FieldName RawBody (lens-db I FieldName C):-
   % In order to support primitive records we call the elaborator, which
   % eventually compiles the match into primitive projections
   std.assert-ok! (coq.elaborate-skeleton RawBody Ty Body) "derive.lens generates illtyped term",
-  (pi P P1 N\ copy (primitive (proj P N)) (primitive (proj P1 N)) :- coq.primitive.projection-unfolded P1 P) => copy Body Body1,
+  ((pi P P1 N\ copy (primitive (proj P N)) (primitive (proj P1 N)) :- coq.primitive.projection-unfolded P1 P) => copy Body Body1),
   coq.env.add-const Name Body1 Ty @transparent! C,
   std.map {std.iota Nparams} (_\r\ r = maximal) Implicits,
   if (Nparams > 0)

apps/derive/elpi/param1.elpi

@@ -97,7 +97,7 @@ reali-match (fun N T B) PRM :- pi x\ not (B x = fun _ _ _), !, do! [
 
 reali-match (fun N T B) PRM :- do! [
   reali T TR,
-  (pi x xR\ reali x xR => reali-match (B x) (BR x xR)),
+  (pi x xR\ (reali x xR ==> reali-match (B x) (BR x xR))),
   coq.name-suffix N 1 N1,
   (pi z \ PRM z = fun N T x\ fun N1 {coq.subst-fun [x] TR} xR\ BR x xR z)
 ].
@@ -164,11 +164,11 @@ dispatch (indt GR) Prefix Clauses :- !, do! [
   LnoR is 2 * Lno,
 
   pi new_name\ sigma KnamesR KtypesR TyR\ (
-    reali Ind (global (indt new_name)) => reali Ty TyR,
-    reali Ind (global (indt new_name)) =>
+    (reali Ind (global (indt new_name)) ==>
+      reali Ty TyR,
       map2 Knames Ktypes (k\ ty\ r\ sigma tyr\
         reali ty tyr, coq.subst-fun [global (indc k)] tyr r)
-      KtypesR,
+      KtypesR),
     map Knames (prefix-indc Prefix) KnamesR,
 
     NewName is Prefix ^ {coq.gref->id (indt GR)},

apps/derive/elpi/projK.elpi

@@ -121,7 +121,7 @@ allK-projs Prefix J JN Paramsno Arity IT K KTy Clauses :- do! [
   J1 is J + 1,
   Name is Prefix ^ {coq.gref->id (indc K)} ^ {any->string J1},
   if (coq.elaborate-skeleton RSkel TyR R ok)
-     (@dropunivs! => coq.env.add-const Name R TyR _ P,
+     ((@dropunivs! => coq.env.add-const Name R TyR _ P),
       Clause = (projK-db K J1 (global (const P)) :- !),
       coq.elpi.accumulate _ "derive.projK.db" (clause _ (before "projK-db:fail") Clause),
       Clauses = [Clause|ClausesRest])

apps/eltac/theories/case.v

@@ -7,7 +7,7 @@ Elpi Accumulate lp:{{
   mk-abstracted-goal ToAbstract Goal  _IndSort Vars _VarsTys Out :-
     std.map2 ToAbstract Vars (t\v\r\ r = copy t v) Subst,
     % Non deterministically we abstract until we obtain a well typed term
-    Subst => copy Goal Out,
+    (Subst ==> copy Goal Out),
     coq.say "trying" {coq.term->string Out},
     coq.typecheck Out _ ok.
 

apps/eltac/theories/clear.v

@@ -27,10 +27,10 @@ Elpi Accumulate lp:{{
   msolve [nabla G] [nabla G1] :- pi x\ msolve [G x] [G1 x].
   msolve [seal  (goal Ctx _ T E ToBeCleared)] [seal (goal Ctx1 _ T E1 [])] :-
     std.map Ctx (drop-body ToBeCleared) Ctx1,
-    @ltacfail! 0 => % this failure can be catch by ltac
-      Ctx1 => % in the new context, do...
-        std.assert-ok! (coq.typecheck-ty T _) "cannot clear since the goal does not typecheck in the new context",
-    Ctx1 => std.assert-ok! (coq.typecheck E1 T) "should not happen", % E1 see all the proof variables (the pi x in the nabla case) and T is OK in Ctx1
+    (@ltacfail! 0 ==> % this failure can be catch by ltac
+      Ctx1 ==> % in the new context, do...
+        std.assert-ok! (coq.typecheck-ty T _) "cannot clear since the goal does not typecheck in the new context"),
+    (Ctx1 ==> std.assert-ok! (coq.typecheck E1 T) "should not happen"), % E1 see all the proof variables (the pi x in the nabla case) and T is OK in Ctx1
     E = {{ lp:E1 : lp:T }}. % we make progress by saying that the old goal/evar is solved by the new one (which has the same type thanks to the line above)
     % note that E = E1 would be "unstable" since elpi could decide to
     % actually do E1 := E, while E = (let `x` T E1 x\x) forces elpi

apps/tc/tests/test.v

@@ -245,7 +245,7 @@ Module HO_9.
   Instance i1 A: c1 (fun x => f (A x) (A x)). Qed.
 
   Elpi Query TC.Solver lp:{{
-    pi F\ sigma T\ decl F `x` {{Type -> Type}} => tc.precomp.instance.is-uvar F => 
+    pi F\ sigma T\ decl F `x` {{Type -> Type}} ==> tc.precomp.instance.is-uvar F ==> 
       tc.precomp.instance {{c1 (fun x => f (lp:F x) (lp:F x))}} T N _ _,
       std.assert! (T = app [{{c1}}, tc.maybe-eta-tm _ _]) "Invalid precompilation".
   }}.

dune

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

elpi/coq-lib-common.elpi

@@ -136,18 +136,18 @@ parse-attributes.aux [] _ [].
 parse-attributes.aux [attribute S (node L)|AS] Prefix R :- 
   append-string Prefix S PS, supported-attribute (att PS attlist), !,
   parse-attributes.aux AS Prefix R1,
-  (pi x\ supported-attribute (att x bool) :- !) => parse-attributes.aux L "" Map,
+  ((pi x\ supported-attribute (att x bool) :- !) ==> parse-attributes.aux L "" Map),
   std.append R1 [get-option PS Map] R.
 parse-attributes.aux [attribute S (node L)|AS] Prefix R :- 
   append-string Prefix S PS, supported-attribute (att PS attmap), !,
   parse-attributes.aux AS Prefix R1,
-  (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map,
+  ((pi x\ supported-attribute (att x string) :- !) ==> parse-attributes.aux L "" Map),
   std.append R1 [get-option PS Map] R.
 parse-attributes.aux [attribute S (node L)|AS] Prefix R :- 
   append-string Prefix S PS, supported-attribute (att PS attlabel), !,
   parse-attributes.aux AS Prefix R1,
   std.map L keep-only-label Ll,
-  (pi x\ supported-attribute (att x bool) :- !) => parse-attributes.aux Ll "" Map,
+  ((pi x\ supported-attribute (att x bool) :- !) ==> parse-attributes.aux Ll "" Map),
   parse-attributes.aux L Prefix R2,
   std.append R1 [get-option PS Map|R2] R.
 parse-attributes.aux [attribute S (node L)|AS] Prefix R :- !,

elpi/coq-lib.elpi

@@ -229,7 +229,7 @@ coq.build-indt-decl-aux (pr GR I) IsInd NUPno 0 Ty Kns KtysNu Params (inductive
   pi i\
     map2 Kns Ktys (gr_name\ ty\ res\
       sigma tmp name\
-      Sub i => copy-arity ty tmp,
+      (Sub i ==> copy-arity ty tmp),
       gr_name = pr _ name,
       res = constructor name tmp)
     (Ks i).
@@ -562,9 +562,9 @@ coq.build-match T Tty RtyF BranchF (match T Rty Bs) :-
   if2 (HD = global (indt GR)) true
       (HD = pglobal (indt GR) I) true
       fail,
-  @uinstance! I => coq.env.indt GR _ Lno _ Arity Kn Kt,
+  (@uinstance! I ==> coq.env.indt GR _ Lno _ Arity Kn Kt),
   take Lno Args LArgs,
-  @uinstance! I => coq.mk-app {coq.env.global (indt GR)} LArgs IndtLArgs,
+  (@uinstance! I ==> coq.mk-app {coq.env.global (indt GR)} LArgs IndtLArgs),
   % Rty
   coq.subst-prod LArgs Arity ArityArgs,
   coq.bind-ind-arity-no-let IndtLArgs ArityArgs RtyF Rty,

elpi/elpi-reduction.elpi

@@ -83,7 +83,7 @@ pred unfold % delta (global constants) + hd-beta
   o:term,                 % body
   o:stack.                % args after hd-beta
 unfold GR none A BO BOC :- coq.env.const GR (some B) _, hd-beta B A BO BOC.
-unfold GR (some I) A BO BOC :- @uinstance! I => coq.env.const GR (some B) _, hd-beta B A BO BOC.
+unfold GR (some I) A BO BOC :- (@uinstance! I ==> coq.env.const GR (some B) _), hd-beta B A BO BOC.
 
 % ensures its first argument is the whd of the second
 pred cache i:term, o:term.

elpi/elpi_elaborator.elpi

@@ -308,7 +308,7 @@ of (sort S) (sort S1) (sort S) :- coq.sort.sup S S1.
 
 of (global GR as X) T X :- coq.env.typeof GR T1, unify-leq T1 T.
 of (pglobal GR I as X) T X :-
-  @uinstance! I => coq.env.typeof GR T1, unify-leq T1 T.
+  (@uinstance! I => coq.env.typeof GR T1), unify-leq T1 T.
 
 of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:elpi.uint63 }} T.
 of (primitive (float64 _) as X) T X :- unify-leq {{ lib:elpi.float64 }} T.