fsetdec: clear dependent hypothesis before anything else (fix #2136).

  Since the tactic fsetdec is doing lots of "clear" and also "subst"
  on equalities, things may go wrong in case of dependencies amongst
  hypothesis. For the moment, we clear all hypothesis that mention
  other hypothesis of sort Prop.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13162 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 0 deletions

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index a87103232..2769c7611 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. *)