diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-26 01:29:33 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-26 01:29:33 +0000 |
| commit | 0919391f43729bf172ab00c8dec9438a0a9f59ab (patch) | |
| tree | 8afd08a9df68b58711da31a14bd2e8ec23b359ba /theories/Lists | |
| parent | 42bb029c878666a7a897ff615acdc60e7f67dd06 (diff) | |
Change Hint Resolve, Immediate to take a global reference as argument
instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/SetoidList.v | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 7d3c383c1..8fd229917 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -101,10 +101,12 @@ Proof. split; induction 1; auto. Qed. (** Results concerning lists modulo [eqA] *) Hypothesis eqA_equiv : Equivalence eqA. +Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv). +Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv). +Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv). -Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv). -Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv). -Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv). +Hint Resolve eqarefl eqatrans. +Hint Immediate eqasym. Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA. @@ -633,7 +635,9 @@ Variable ltA : A -> A -> Prop. Hypothesis ltA_strorder : StrictOrder ltA. Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA. -Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder). +Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder). + +Hint Resolve sotrans. Notation InfA:=(lelistA ltA). Notation SortA:=(sort ltA). @@ -821,7 +825,7 @@ Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. Proof. -clear ltA ltA_compat ltA_strorder. +clear sotrans ltA ltA_strorder ltA_compat. intros; do 2 rewrite InA_alt; intuition. destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. |