From b02da518c51456b003c61f9775050fbfe6090629 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 25 Oct 2009 07:36:43 +0000 Subject: Improved the treatment of Local/Global options (noneffective Local on Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/DecidableType2.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'theories') diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index 61fd743dc..b1cd5bfa5 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -64,8 +64,8 @@ Module KeyDecidableType(D:DecidableType). Definition eqke (p p':key*elt) := eq (fst p) (fst p') /\ (snd p) = (snd p'). - Global Hint Unfold eqk eqke. - Global Hint Extern 2 (eqke ?a ?b) => split. + Hint Unfold eqk eqke. + Hint Extern 2 (eqke ?a ?b) => split. (* eqke is stricter than eqk *) @@ -88,19 +88,19 @@ Module KeyDecidableType(D:DecidableType). red; unfold eqke; intuition; [ eauto | congruence ]. Qed. - Global Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv). - Global Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv). - Global Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv). - Global Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv). - Global Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv). - Global Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv). + Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv). + Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv). + Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv). + Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv). Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. Qed. - Global Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk. Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. @@ -110,7 +110,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. - Global Hint Unfold MapsTo In. + Hint Unfold MapsTo In. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) -- cgit v1.2.3