Compat with Hint Constants Opaque : rewrite (coq/coq#15588)

SkySkimmer · Feb 3, 2022 · 1d196ca · 1d196ca
1 parent cd3bc92
commit 1d196ca
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 2 deletions.
diff --git a/pcuic/theories/Conversion/PCUICInstConv.v b/pcuic/theories/Conversion/PCUICInstConv.v
@@ -1045,6 +1045,7 @@ Proof.
     rewrite !(lift_extended_subst _ 1).
     rewrite map_map_compose.
     setoid_rewrite up_Upn; setoid_rewrite lift0_inst; setoid_rewrite inst_assoc.
+    rewrite <-(Nat.add_1_l (context_assumptions Γ)).
     setoid_rewrite (Upn_Upn 1); setoid_rewrite shiftn_Upn;
     setoid_rewrite <- up_Upn; setoid_rewrite <-inst_assoc.
     setoid_rewrite <- lift0_inst.

diff --git a/pcuic/theories/Conversion/PCUICRenameConv.v b/pcuic/theories/Conversion/PCUICRenameConv.v
@@ -917,6 +917,7 @@ Proof.
   - f_equal; auto.
     rewrite !(lift_extended_subst _ 1).
     rewrite map_map_compose.
+    rewrite <-Nat.add_1_l.
     setoid_rewrite <- (shiftn_add 1 (context_assumptions Γ)).
     setoid_rewrite rename_shiftn.
     rewrite -map_map_compose. now f_equal.

diff --git a/pcuic/theories/Syntax/PCUICOnFreeVars.v b/pcuic/theories/Syntax/PCUICOnFreeVars.v
@@ -970,6 +970,7 @@ Lemma on_free_vars_ctx_on_ctx_free_vars {P Γ} :
 Proof.
   induction Γ => /= //.
   rewrite /on_free_vars_ctx /= alli_app /= andb_true_r; len.
+  rewrite <-(Nat.add_1_l #|Γ|).
   setoid_rewrite <-(shiftnP_add 1 #|Γ|); rewrite addnP_shiftnP andb_comm.
   f_equal. rewrite /on_free_vars_ctx in IHΓ. rewrite -IHΓ.
   rewrite (alli_shift _ _ 1) /=.

diff --git a/template-coq/theories/Universes.v b/template-coq/theories/Universes.v
@@ -1117,7 +1117,8 @@ End ConstraintType.
 
 Module UnivConstraint.
   Definition t : Set := Level.t * ConstraintType.t * Level.t.
-
+  Global Hint Transparent t : rewrite. (* needed due to inconsistent inlining between t itself and eq *)
+
   Definition eq : t -> t -> Prop := eq.
   Definition eq_equiv : Equivalence eq := _.
 
@@ -1673,6 +1674,7 @@ Definition fresh_level : Level.t. exact Level.lzero. Qed.
 (** Substitutable type *)
 
 Class UnivSubst A := subst_instance : Instance.t -> A -> A.
+Global Hint Transparent subst_instance : rewrite.
 
 Notation "x @[ u ]" := (subst_instance u x) (at level 3, 
   format "x @[ u ]").

diff --git a/template-coq/theories/common/uGraph.v b/template-coq/theories/common/uGraph.v
@@ -25,6 +25,7 @@ Derive NoConfusion for universes.
 Module VariableLevel.
   Inductive t_ := Level (_ : string) | Var (_ : nat).
   Definition t := t_.
+  Global Hint Transparent t : rewrite.
 
   Declare Scope var_level.
   Delimit Scope var_level with var_level.
@@ -148,6 +149,7 @@ Module GoodConstraint.
   | gc_le_var_set : nat -> nat -> t_.
   Derive NoConfusion for t_.
   Definition t : Set := t_.
+  Global Hint Transparent t : rewrite.
   Definition eq : t -> t -> Prop := Logic.eq.
   Definition eq_refl := @eq_refl t.
   Definition eq_sym := @eq_sym t.
@@ -2424,7 +2426,7 @@ Section AddLevelsCstrs.
     (exists c, option_edge_of_level c = Some e /\ VSet.In c x) \/ EdgeSet.In e g.
   Proof.
     rewrite /add_level_edges VSet.fold_spec.
-    setoid_rewrite (VSetFact.elements_iff x). setoid_rewrite InA_In_eq at 2.
+    setoid_rewrite (VSetFact.elements_iff x). setoid_rewrite InA_In_eq.
     induction (VSet.elements x) in g |- *; simpl.
     intuition auto. now destruct H0 as [c [_ F]].
     rewrite {}IHl.