Subtac bug fix, add list take example.

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

1 files changed, 18 insertions, 1 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index f5115812ac..aa1d0ff388 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -44,6 +44,23 @@ end.
 
 Ltac destruct_exists := repeat (destruct_one_pair) .
 
-Ltac subtac_simpl := simpl ; intros ; destruct_exists.
+Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in *.
+
+(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
+Ltac destruct_call f :=
+  match goal with
+    | H : ?T |- _  =>
+      match T with
+         context [f ?x ?y ?z] => destruct (f x y z)
+       | context [f ?x ?y] => destruct (f x y)
+       | context [f ?x] => destruct (f x)        
+      end
+    | |- ?T  =>
+      match T with
+        context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n
+        | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n
+        | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n
+      end
+    end.
 
 Extraction Inline proj1_sig.