Legacy: adapt to coq/coq#18325 (#1750)

mit-plv · Nov 23, 2023 · e82ae48 · e82ae48
1 parent 505351b
commit e82ae48
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 56 deletions.
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
@@ -9,34 +9,7 @@ Module Export Hints1.
   Export Crypto.Algebra.Hierarchy.Hints.
   Export Crypto.Algebra.Ring.Hints.
   Export Crypto.Algebra.IntegralDomain.Hints.
-  Global Existing Instances
-         Ncring_tac.Ifind0
-         Ncring_tac.Iclosed_nil
-         Ncring_tac.Iclosed_cons
-         Ncring_tac.reify_zero
-         Ncring_tac.reify_one
-         Ncring_tac.reify_add
-         Ncring_tac.reify_sub
-         Ncring_tac.reify_opp
-         Ncring_tac.reify_nil
-         Ncring_tac.reify_cons
-  .
-  Global Existing Instances
-         Ncring_tac.IfindS
-         Ncring_tac.reify_pow
-  | 1.
-  Global Existing Instances
-         Ncring_tac.reify_mul_ext
-  | 9.
-  Global Existing Instances
-         Ncring_tac.reify_mul
-  | 10.
-  Global Existing Instances
-         Ncring_tac.reifyZ0
-         Ncring_tac.reifyZpos
-         Ncring_tac.reifyZneg
-  | 11.
-  Global Existing Instance Ncring_tac.reify_var | 100.
+  Export (hints) Ncring_tac.
 End Hints1.
 
 Section Field.

diff --git a/src/Algebra/Nsatz.v b/src/Algebra/Nsatz.v
@@ -175,34 +175,7 @@ Ltac nsatz_contradict :=
 
 Module Export Hints.
   Export Crypto.Util.FixCoqMistakes.
-  Global Existing Instances
-         Ncring_tac.Ifind0
-         Ncring_tac.Iclosed_nil
-         Ncring_tac.Iclosed_cons
-         Ncring_tac.reify_zero
-         Ncring_tac.reify_one
-         Ncring_tac.reify_add
-         Ncring_tac.reify_sub
-         Ncring_tac.reify_opp
-         Ncring_tac.reify_nil
-         Ncring_tac.reify_cons
-  .
-  Global Existing Instances
-         Ncring_tac.IfindS
-         Ncring_tac.reify_pow
-  | 1.
-  Global Existing Instances
-         Ncring_tac.reify_mul_ext
-  | 9.
-  Global Existing Instances
-         Ncring_tac.reify_mul
-  | 10.
-  Global Existing Instances
-         Ncring_tac.reifyZ0
-         Ncring_tac.reifyZpos
-         Ncring_tac.reifyZneg
-  | 11.
-  Global Existing Instance Ncring_tac.reify_var | 100.
+  Export (hints) Ncring_tac.
   Global Existing Instances
          Ncring_initial.Zops
          Ncring_initial.Zr