diff options
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetDecide.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index 1161739ed..1646ea7fa 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -344,6 +344,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. *) @@ -403,7 +416,7 @@ the above form: propositions of interest. *) Inductive MSet_elt_Prop : Prop -> Prop := - | eq_Prop : forall (S : Set) (x y : S), + | eq_Prop : forall (S : Type) (x y : S), MSet_elt_Prop (x = y) | eq_elt_prop : forall x y, MSet_elt_Prop (E.eq x y) @@ -662,6 +675,9 @@ the above form: [intros] to leave us with a goal of [~ P] than a goal of [False]. *) fold any not; intros; + (** We remove dependencies to logical hypothesis. This way, + later "clear" will work nicely (see bug #2136) *) + no_logical_interdep; (** Now we decompose conjunctions, which will allow the [discard_nonMSet] and [assert_decidability] tactics to do a much better job. *) |