From 7e38b6627caaab7d19c4fc0ee542a67d9f8970c2 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 24 Oct 2016 17:28:51 +0200 Subject: Remove v62 from stdlib. This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore. --- theories/Logic/Eqdep.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Logic') diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index f3a2783e1..5ef86b8e7 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -33,5 +33,5 @@ Export EqdepTheory. (** Exported hints *) -Hint Resolve eq_dep_eq: eqdep v62. +Hint Resolve eq_dep_eq: eqdep. Hint Resolve inj_pair2 inj_pairT2: eqdep. -- cgit v1.2.3