Restrict the "simp" hint database to not unfold constants by default,…

… for efficiency and backward compatibility.
mattam82 · May 23, 2024 · fec3cbb · fec3cbb
1 parent 9597598
commit fec3cbb
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/examples/AlmostFull.v b/examples/AlmostFull.v
@@ -842,7 +842,7 @@ Section SCT.
     graphs_relation (compose_family g g') x y.
   Proof.
     intros gxz gzy.
-    induction g in g', x, y, z, gxz, gzy |- *; simp compose_family.
+    induction g in g', x, y, z, gxz, gzy |- *; simp compose_family; auto.
     unfold graphs_relation in gxz.
     simpl in gxz. destruct gxz.
     unfold graphs_relation.

diff --git a/theories/Init.v b/theories/Init.v
@@ -152,6 +152,9 @@ Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
   solve recursive calls obligations or during [simp] calls. *)
 
 Create HintDb simp discriminated.
+Hint Variables Opaque : simp.
+Hint Constants Opaque : simp.
+Hint Projections Opaque : simp.
 
 (** Forward reference to an internal tactic to unfold well-founded fixpoints *)
 Ltac unfold_recursor := fail "Equations.Init.unfold_recursor has not been bound yet".