Separate Tactics in subtac.

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

2 files changed, 46 insertions, 41 deletions

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index 25d8d8319d..dae389ce30 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -20,3 +20,47 @@ Ltac induction_with_subterms c c' H :=
   set(z := c') ; assert(w:z = c') by reflexivity ;
   rewrite <- y in H ; rewrite <- w in H ; 
   induction H ; subst).
+
+
+Ltac destruct_one_pair :=
+ match goal with
+ | [H : (ex _) |- _] => destruct H
+ | [H : (ex2 _) |- _] => destruct H
+ | [H : (sig _) |- _] => destruct H
+ | [H : (_ /\ _) |- _] => destruct H
+end.
+
+Ltac destruct_exists := repeat (destruct_one_pair) .
+
+(* 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.
+
+Ltac myinjection :=
+      let tac H := inversion H ; subst ; clear H in
+        match goal with
+          | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
+          | [ H : ?f ?a ?b = ?f' ?a' ?b'  |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
+          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
+          | _ => idtac
+        end.
+
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 6e1a8ee44f..4ef4f3eced 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -1,3 +1,5 @@
+Require Export Coq.subtac.SubtacTactics.
+
 Set Implicit Arguments.
 
 Notation "'fun' { x : A | P } => Q" :=
@@ -41,51 +43,10 @@ induction t.
  simpl ; auto.
 Qed.
 
-Ltac destruct_one_pair :=
- match goal with
- | [H : (ex _) |- _] => destruct H
- | [H : (ex2 _) |- _] => destruct H
- | [H : (sig _) |- _] => destruct H
- | [H : (_ /\ _) |- _] => destruct H
-end.
-
-Ltac destruct_exists := repeat (destruct_one_pair) .
 
 Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; 
   try (solve [ red ; intros ; discriminate ]) ; auto with arith.  
 
-(* 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.
-
-Ltac myinjection :=
-      let tac H := inversion H ; subst ; clear H in
-        match goal with
-          | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
-          | [ H : ?f ?a ?b = ?f' ?a' ?b'  |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
-          | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
-          | _ => idtac
-        end.
-
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].