Merge pull request #70 from ppedrot/hint-locality-error

Adapt w.r.t. coq/coq#16004.

BigN/Nbasic.v

@@ -501,7 +501,9 @@ Module Type NAbstract.
 (** The domains: a sequence of [Z/nZ] structures *)
 
 Parameter dom_t : nat -> univ_of_cycles.
+#[global]
 Declare Instance dom_op n : ZnZ.Ops (dom_t n).
+#[global]
 Declare Instance dom_spec n : ZnZ.Specs (dom_op n).
 
 Axiom digits_dom_op : forall n,

BigN/gen/NMake_gen.ml

@@ -71,13 +71,13 @@ pr " (** * The operation type classes for the word types *)
 
 pr " Local Notation w0_op := W0.ops.";
 for i = 1 to min 3 size do
-  pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1)
+  pr " #[global] Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops w%i_op." i i (i-1)
 done;
 for i = 4 to size do
-  pr " Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1)
+  pr " #[global] Instance w%i_op : ZnZ.Ops w%i := mk_zn2z_ops_karatsuba w%i_op." i i (i-1)
 done;
 for i = size+1 to size+3 do
-  pr " Instance w%i_op : ZnZ.Ops (word w%i %i) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1)
+  pr " #[global] Instance w%i_op : ZnZ.Ops (word w%i %i) := mk_zn2z_ops_karatsuba w%i_op." i size (i-size) (i-1)
 done;
 pr "";
 
@@ -105,7 +105,7 @@ pr "";
   pr "";
   pr " Definition make_op_list := dmemo_list _ omake_op.";
   pr "";
-  pr " Instance make_op n : ZnZ.Ops (word w%i (S n))" size;
+  pr " #[global] Instance make_op n : ZnZ.Ops (word w%i (S n))" size;
   pr "  := dmemo_get _ omake_op n make_op_list.";
   pr "";
 
@@ -161,7 +161,7 @@ pr
   pr "";
 
 pr
-" Instance dom_op n : ZnZ.Ops (dom_t n) | 10.
+" #[global] Instance dom_op n : ZnZ.Ops (dom_t n) | 10.
  Proof.
   do_size (destruct n; [simpl;auto with *|]).
   unfold dom_t. auto with *.
@@ -279,28 +279,28 @@ pr
 ";
 
   if size <> 0 then
-  pr " Typeclasses Opaque %s." (iter_name 1 size "w" "");
+  pr " #[global] Typeclasses Opaque %s." (iter_name 1 size "w" "");
   pr "";
 
-  pr " Instance w0_spec: ZnZ.Specs w0_op := W0.specs.";
+  pr " #[global] Instance w0_spec: ZnZ.Specs w0_op := W0.specs.";
   for i = 1 to min 3 size do
-    pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs w%i_spec." i i (i-1)
+    pr " #[global] Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs w%i_spec." i i (i-1)
   done;
   for i = 4 to size do
-    pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
+    pr " #[global] Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." i i (i-1)
   done;
-  pr " Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." (size+1) (size+1) size;
+  pr " #[global] Instance w%i_spec: ZnZ.Specs w%i_op := mk_zn2z_specs_karatsuba w%i_spec." (size+1) (size+1) size;
 
 
 pr "
- Instance wn_spec (n:nat) : ZnZ.Specs (make_op n).
+ #[global] Instance wn_spec (n:nat) : ZnZ.Specs (make_op n).
  Proof.
   induction n.
   rewrite make_op_omake; simpl; auto with *.
   rewrite make_op_S. exact (mk_zn2z_specs_karatsuba IHn).
  Qed.
 
- Instance dom_spec n : ZnZ.Specs (dom_op n) | 10.
+ #[global] Instance dom_spec n : ZnZ.Specs (dom_op n) | 10.
  Proof.
   do_size (destruct n; auto with *). apply wn_spec.
  Qed.

BigNumPrelude.v

@@ -49,20 +49,23 @@ Definition Z_div_plus_l a b c H := Zdiv.Z_div_plus_full_l a b c (Zlt0_not_eq _ H
 
 (* Automation *)
 
+#[global]
 Hint Extern 2 (Z.le _ _) =>
  (match goal with
    |- Zpos _ <= Zpos _ => exact (eq_refl _)
 |   H: _ <=  ?p |- _ <= ?p => apply Z.le_trans with (2 := H)
 |   H: _ <  ?p |- _ <= ?p => apply Z.lt_le_incl; apply Z.le_lt_trans with (2 := H)
   end) : core.
 
+#[global]
 Hint Extern 2 (Z.lt _ _) =>
  (match goal with
    |- Zpos _ < Zpos _ => exact (eq_refl _)
 |      H: _ <=  ?p |- _ <= ?p => apply Z.lt_le_trans with (2 := H)
 |   H: _ <  ?p |- _ <= ?p => apply Z.le_lt_trans with (2 := H)
   end) : core.
 
+#[global]
 Hint Resolve Z.lt_gt Z.le_ge Z_div_pos: zarith.
 
 (**************************************
@@ -123,6 +126,7 @@ Theorem mult_add_ineq3: forall x y c cross beta,
    0 <= x * y + (c*beta + cross) < beta^2.
  Proof. nia. Qed.
 
+#[global]
 Hint Rewrite Z.mul_1_r Z.mul_0_r Z.mul_1_l Z.mul_0_l Z.add_0_l Z.add_0_r Z.sub_0_r: rm10.
 
 

BigQ/QMake.v

@@ -84,6 +84,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
    | _ => idtac
   end.
 
+#[global]
  Hint Rewrite
   Z.add_0_r Z.add_0_l Z.mul_0_r Z.mul_0_l Z.mul_1_r Z.mul_1_l
   ZZ.spec_0 NN.spec_0 ZZ.spec_1 NN.spec_1 ZZ.spec_m1 ZZ.spec_opp
@@ -346,6 +347,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  destr_eqb; auto using Qeq_refl, spec_norm.
  Qed.
 
+#[global]
  Instance strong_spec_add_norm x y
    `(Reduced x, Reduced y) : Reduced (add_norm x y).
  Proof.
@@ -379,6 +381,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  intros; rewrite strong_spec_opp; red; auto.
  Qed.
 
+#[global]
  Instance strong_spec_opp_norm q `(Reduced q) : Reduced (opp q).
  Proof.
  unfold Reduced; intros.
@@ -402,6 +405,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite spec_opp; ring.
  Qed.
 
+#[global]
  Instance strong_spec_sub_norm x y
   `(Reduced x, Reduced y) : Reduced (sub_norm x y).
  Proof.
@@ -559,6 +563,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite Zgcd_div_swap0; lia.
  Qed.
 
+#[global]
  Instance strong_spec_mul_norm_Qz_Qq z n d :
    forall `(Reduced (Qq n d)), Reduced (mul_norm_Qz_Qq z n d).
  Proof.
@@ -644,6 +649,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring.
  Qed.
 
+#[global]
  Instance strong_spec_mul_norm x y :
   forall `(Reduced x, Reduced y), Reduced (mul_norm x y).
  Proof.
@@ -824,6 +830,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  lia.
  Qed.
 
+#[global]
  Instance strong_spec_inv_norm x : Reduced x -> Reduced (inv_norm x).
  Proof.
  unfold Reduced.
@@ -895,6 +902,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  apply spec_inv_norm; auto.
  Qed.
 
+#[global]
  Instance strong_spec_div_norm x y
    `(Reduced x, Reduced y) : Reduced (div_norm x y).
  Proof.
@@ -958,6 +966,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
    now rewrite NN.spec_pow_pos.
  Qed.
 
+#[global]
  Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p).
  Proof.
  destruct x as [z | n d]; simpl; intros.
@@ -1011,6 +1020,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl.
  Qed.
 
+#[global]
  Instance strong_spec_power_norm x z :
    Reduced x -> Reduced (power_norm x z).
  Proof.
@@ -1039,6 +1049,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold of_Qc; rewrite strong_spec_of_Q; auto.
  Qed.
 
+#[global]
  Instance strong_spec_of_Qc_bis q : Reduced (of_Qc q).
  Proof.
  intros; red; rewrite strong_spec_red, strong_spec_of_Qc.

CyclicDouble/DoubleCyclic.v

@@ -955,7 +955,9 @@ End MulAdd.
 
 Module DoubleCyclic (C:CyclicType) <: CyclicType.
  Definition t := zn2z C.t.
+#[global]
  Instance ops : ZnZ.Ops t := mk_zn2z_ops.
+#[global]
  Instance specs : ZnZ.Specs ops := mk_zn2z_specs.
 End DoubleCyclic.
 

SpecViaQ/QSig.v

@@ -96,6 +96,7 @@ Module QProperties (Import Q : QType').
 
 (** Conversion to Q *)
 
+#[global]
 Hint Rewrite
  spec_red spec_compare spec_eq_bool spec_min spec_max
  spec_add spec_sub spec_opp spec_mul spec_square spec_inv spec_div
@@ -114,26 +115,43 @@ Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy.
 
 Local Obligation Tactic := solve_wd2 || solve_wd1.
 
+#[global]
 Instance : Measure to_Q := {}.
+#[global]
 Instance eq_equiv : Equivalence eq.
 Proof.
   change eq with (RelCompFun Qeq to_Q); apply _.
 Defined.
 
+#[global]
 Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
+#[global]
 Program Instance le_wd : Proper (eq==>eq==>iff) le.
+#[global]
 Program Instance red_wd : Proper (eq==>eq) red.
+#[global]
 Program Instance compare_wd : Proper (eq==>eq==>Logic.eq) compare.
+#[global]
 Program Instance eq_bool_wd : Proper (eq==>eq==>Logic.eq) eq_bool.
+#[global]
 Program Instance min_wd : Proper (eq==>eq==>eq) min.
+#[global]
 Program Instance max_wd : Proper (eq==>eq==>eq) max.
+#[global]
 Program Instance add_wd : Proper (eq==>eq==>eq) add.
+#[global]
 Program Instance sub_wd : Proper (eq==>eq==>eq) sub.
+#[global]
 Program Instance opp_wd : Proper (eq==>eq) opp.
+#[global]
 Program Instance mul_wd : Proper (eq==>eq==>eq) mul.
+#[global]
 Program Instance square_wd : Proper (eq==>eq) square.
+#[global]
 Program Instance inv_wd : Proper (eq==>eq) inv.
+#[global]
 Program Instance div_wd : Proper (eq==>eq==>eq) div.
+#[global]
 Program Instance power_wd : Proper (eq==>Logic.eq==>eq) power.
 
 (** Let's implement [HasCompare] *)
@@ -144,6 +162,7 @@ Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed.
 (** Let's implement [TotalOrder] *)
 
 Definition lt_compat := lt_wd.
+#[global]
 Instance lt_strorder : StrictOrder lt.
 Proof.
   change lt with (RelCompFun Qlt to_Q); apply _.

SpecViaZ/NSigNAxioms.v

@@ -12,6 +12,7 @@ Require Import ZArith OrdersFacts Nnat NAxioms NSig Lia.
 
 Module NTypeIsNAxioms (Import NN : NType').
 
+#[global]
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
@@ -26,13 +27,19 @@ Ltac omega_pos n := generalize (spec_pos n); lia.
 
 Local Obligation Tactic := ncongruence.
 
+#[global]
 Instance eq_equiv : Equivalence eq.
 Proof. split; ncongruence. Qed.
 
+#[global]
 Program Instance succ_wd : Proper (eq==>eq) succ.
+#[global]
 Program Instance pred_wd : Proper (eq==>eq) pred.
+#[global]
 Program Instance add_wd : Proper (eq==>eq==>eq) add.
+#[global]
 Program Instance sub_wd : Proper (eq==>eq==>eq) sub.
+#[global]
 Program Instance mul_wd : Proper (eq==>eq==>eq) mul.
 
 Theorem pred_succ : forall n, pred (succ n) == n.
@@ -164,26 +171,31 @@ Qed.
 
 Include BoolOrderFacts NN NN NN [no inline].
 
+#[global]
 Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
 intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
+#[global]
 Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
 Proof.
 intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
+#[global]
 Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
 Proof.
 intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
+#[global]
 Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
 Proof.
 intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
+#[global]
 Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
 Proof.
 intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
@@ -223,6 +235,7 @@ Qed.
 
 (** Power *)
 
+#[global]
 Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
 
 Lemma pow_0_r : forall a, a^0 == 1.
@@ -313,7 +326,9 @@ Qed.
 
 (** Div / Mod *)
 
+#[global]
 Program Instance div_wd : Proper (eq==>eq==>eq) div.
+#[global]
 Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
 Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b).
@@ -364,6 +379,7 @@ Qed.
 
 (** Bitwise operations *)
 
+#[global]
 Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
 
 Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true.
@@ -447,6 +463,7 @@ Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) :=
   N.peano_rect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n).
 Arguments recursion [A] a f n.
 
+#[global]
 Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.