adapt to MC#1319

math-comp · Jan 16, 2025 · 16aba2a · 16aba2a
1 parent 12e9b64
commit 16aba2a
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 10 deletions.
diff --git a/theories/common.elpi b/theories/common.elpi
@@ -91,40 +91,44 @@ register-instance Scope DbName Proj Pat Pred :- std.do! [
 
 pred canonical-init i:scope, i:id.
 canonical-init Scope DbName :- std.do! [
+	(coq.locate-all "GRing.PzSemiRing.sort" [loc-gref SemiRing| _ ]; SemiRing = {{:gref GRing.SemiRing.sort }}),
+	(coq.locate-all "GRing.ComPzSemiRing.sort" [loc-gref ComSemiRing| _ ]; ComSemiRing = {{:gref GRing.ComSemiRing.sort }}),
+	(coq.locate-all "GRing.PzRing.sort" [loc-gref Ring| _ ]; Ring = {{:gref GRing.Ring.sort }}),
+	(coq.locate-all "GRing.ComPzRing.sort" [loc-gref ComRing| _ ]; ComRing = {{:gref GRing.ComRing.sort }}),
   register-instance Scope DbName
     {{:gref GRing.Nmodule.sort }} {{:gref nat }} canonical-nat-nmodule,
   register-instance Scope DbName
-    {{:gref GRing.SemiRing.sort }} {{:gref nat }} canonical-nat-semiring,
+    SemiRing {{:gref nat }} canonical-nat-semiring,
   register-instance Scope DbName
-    {{:gref GRing.ComSemiRing.sort }} {{:gref nat }} canonical-nat-comsemiring,
+    ComSemiRing {{:gref nat }} canonical-nat-comsemiring,
   register-instance Scope DbName
     {{:gref GRing.Nmodule.sort }} {{:gref N }} canonical-N-nmodule,
   register-instance Scope DbName
-    {{:gref GRing.SemiRing.sort }} {{:gref N }} canonical-N-semiring,
+    SemiRing {{:gref N }} canonical-N-semiring,
   register-instance Scope DbName
-    {{:gref GRing.ComSemiRing.sort }} {{:gref N }} canonical-N-comsemiring,
+    ComSemiRing {{:gref N }} canonical-N-comsemiring,
   register-instance Scope DbName
     {{:gref GRing.Nmodule.sort }} {{:gref int }} canonical-int-nmodule,
   register-instance Scope DbName
     {{:gref GRing.Zmodule.sort }} {{:gref int }} canonical-int-zmodule,
   register-instance Scope DbName
-    {{:gref GRing.SemiRing.sort }} {{:gref int }} canonical-int-semiring,
+    SemiRing {{:gref int }} canonical-int-semiring,
   register-instance Scope DbName
-    {{:gref GRing.Ring.sort }} {{:gref int }} canonical-int-ring,
+    Ring {{:gref int }} canonical-int-ring,
   register-instance Scope DbName
-    {{:gref GRing.ComRing.sort }} {{:gref int }} canonical-int-comring,
+    ComRing {{:gref int }} canonical-int-comring,
   register-instance Scope DbName
     {{:gref GRing.UnitRing.sort }} {{:gref int }} canonical-int-unitring,
   register-instance Scope DbName
     {{:gref GRing.Nmodule.sort }} {{:gref Z }} canonical-Z-nmodule,
   register-instance Scope DbName
     {{:gref GRing.Zmodule.sort }} {{:gref Z }} canonical-Z-zmodule,
   register-instance Scope DbName
-    {{:gref GRing.SemiRing.sort }} {{:gref Z }} canonical-Z-semiring,
+    SemiRing {{:gref Z }} canonical-Z-semiring,
   register-instance Scope DbName
-    {{:gref GRing.Ring.sort }} {{:gref Z }} canonical-Z-ring,
+    Ring {{:gref Z }} canonical-Z-ring,
   register-instance Scope DbName
-    {{:gref GRing.ComRing.sort }} {{:gref Z }} canonical-Z-comring,
+    ComRing {{:gref Z }} canonical-Z-comring,
   register-instance Scope DbName
     {{:gref GRing.UnitRing.sort }} {{:gref Z }} canonical-Z-unitring ].
 

diff --git a/theories/common.v b/theories/common.v
@@ -12,6 +12,10 @@ Unset Printing Implicit Defensive.
 
 Local Open Scope ring_scope.
 
+Notation semiRingType := (ltac:(exact pzSemiRingType || exact semiRingType)).
+Notation ringType := (ltac:(exact pzRingType || exact ringType)).
+Notation comRingType := (ltac:(exact comPzRingType || exact comRingType)).
+
 Implicit Types (V : nmodType) (R : semiRingType) (F : fieldType).
 
 (* Some basic facts about `Decimal.uint` and `Hexadecimal.uint`               *)