From 16aba2aca5ef843aa44e50b9576e3915e3ab7812 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Thu, 16 Jan 2025 15:04:30 +0100
Subject: [PATCH] adapt to MC#1319

---
 theories/common.elpi | 24 ++++++++++++++----------
 theories/common.v    |  4 ++++
 2 files changed, 18 insertions(+), 10 deletions(-)

diff --git a/theories/common.elpi b/theories/common.elpi
index b0a1a11..d3e070b 100644
--- a/theories/common.elpi
+++ b/theories/common.elpi
@@ -91,28 +91,32 @@ 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
@@ -120,11 +124,11 @@ canonical-init Scope DbName :- std.do! [
   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
index 1a90818..2726d1d 100644
--- 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`               *)