aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Specif.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Specif.v')
-rw-r--r--theories/Init/Specif.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d1038186e..9fc00e80c 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -299,7 +299,7 @@ Proof.
apply (h2 h1).
Defined.
-Hint Resolve left right inleft inright: core v62.
+Hint Resolve left right inleft inright: core.
Hint Resolve exist exist2 existT existT2: core.
(* Compatibility *)