diff options
| -rw-r--r-- | theories/FSets/FSetDecide.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index a871032322..2769c76116 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.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. *) @@ -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_nonFSet] and [assert_decidability] tactics to do a much better job. *) |