revert to tac_in_term with elpi

theories/common.v

@@ -12,18 +12,29 @@ Unset Printing Implicit Defensive.
 
 Local Open Scope ring_scope.
 
-Elpi Command AddRingNotations.
-Elpi Query lp:{{
-  (coq.locate-all "pzSemiRingType" [loc-gref SemiRingType|_];
-      SemiRingType = {{:gref semiRingType }}),
-  coq.notation.add-abbreviation "semiRingType" 0 (global SemiRingType) tt _. 
-  (coq.locate-all "pzRingType" [loc-gref RingType|_];
-      RingType = {{:gref ringType }}),
-  coq.notation.add-abbreviation "ringType" 0 (global RingType) tt _. 
-  (coq.locate-all "comPzRingType" [loc-gref ComRingType|_];
-      ComRingType = {{:gref comRingType }}),
-  coq.notation.add-abbreviation "comRingType" 0 (global ComRingType) tt _. 
+Elpi Tactic semiRingType_tac.
+Elpi Accumulate lp:{{
+  solve G Gs :-
+    (coq.locate-all "pzSemiRingType" [loc-gref C|_]; C = {{:gref semiRingType }}),
+    refine (global C) G Gs.
 }}.
+Notation semiRingType := (ltac:(elpi semiRingType_tac)).
+
+Elpi Tactic ringType_tac.
+Elpi Accumulate lp:{{
+  solve G Gs :-
+    (coq.locate-all "pzRingType" [loc-gref C|_]; C = {{:gref ringType }}),
+    refine (global C) G Gs.
+}}.
+Notation ringType := (ltac:(elpi ringType_tac)).
+
+Elpi Tactic comRingType_tac.
+Elpi Accumulate lp:{{
+  solve G Gs :-
+    (coq.locate-all "comPzRingType" [loc-gref C|_]; C = {{:gref comRingType }}),
+    refine (global C) G Gs.
+}}.
+Notation comRingType := (ltac:(elpi comRingType_tac)).
 
 Implicit Types (V : nmodType) (R : semiRingType) (F : fieldType).