From 405885980b4a7a7eeb8d26cd5a7ad0f132ac6388 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 17 Jun 2010 18:51:23 +0000
Subject: 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
---
 theories/FSets/FSetDecide.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

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. *)
-- 
cgit v1.2.3