diff options
Diffstat (limited to 'theories/FSets/FSetDecide.v')
| -rw-r--r-- | theories/FSets/FSetDecide.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 06b4e028..f84d8f58 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetDecide.v 11699 2008-12-18 11:49:08Z letouzey $ *) +(* $Id: FSetDecide.v 13199 2010-06-25 22:36:22Z letouzey $ *) (**************************************************************) (* FSetDecide.v *) @@ -346,6 +346,19 @@ the above form: (** ** Generic Tactics We begin by defining a few generic, useful tactics. *) + (** remove logical hypothesis inter-dependencies (fix #2136). *) + + Ltac no_logical_interdep := + match goal with + | H : ?P |- _ => + match type of P with + | Prop => + match goal with H' : context [ H ] |- _ => clear dependent H' end + | _ => fail + end; no_logical_interdep + | _ => idtac + end. + (** [if t then t1 else t2] executes [t] and, if it does not fail, then [t1] will be applied to all subgoals produced. If [t] fails, then [t2] is executed. *) @@ -405,7 +418,7 @@ the above form: propositions of interest. *) Inductive FSet_elt_Prop : Prop -> Prop := - | eq_Prop : forall (S : Set) (x y : S), + | eq_Prop : forall (S : Type) (x y : S), FSet_elt_Prop (x = y) | eq_elt_prop : forall x y, FSet_elt_Prop (E.eq x y) @@ -660,6 +673,9 @@ the above form: Ltac fsetdec := (** We first unfold any occurrences of [iff]. *) unfold iff in *; + (** We remove dependencies to logical hypothesis. This way, + later "clear" will work nicely (see bug #2136) *) + no_logical_interdep; (** We fold occurrences of [not] because it is better for [intros] to leave us with a goal of [~ P] than a goal of [False]. *) |