Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a bit broken

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

3 files changed, 26 insertions, 7 deletions

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index e1c48769c..eac46751e 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -24,19 +24,37 @@ Ltac induction_with_subterms c c' H :=
 
 Ltac destruct_one_pair :=
  match goal with
-   | [H : (ex2 _) |- _] => destruct H
    | [H : (_ /\ _) |- _] => destruct H
    | [H : prod _ _ |- _] => destruct H
  end.
 
+Ltac destruct_pairs := repeat (destruct_one_pair).
+
 Ltac destruct_one_ex :=
   let tac H := let ph := fresh "H" in destruct H as [H ph] in
     match goal with
       | [H : (ex _) |- _] => tac H
       | [H : (sig ?P) |- _ ] => tac H
+      | [H : (ex2 _) |- _] => tac H
     end.
 
-Ltac destruct_exists := repeat (destruct_one_pair || destruct_one_ex).
+Ltac destruct_exists := repeat (destruct_one_ex).
+
+Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
+
+Ltac on_last_hyp tac := 
+  match goal with
+    [ H : _ |- _ ] => tac H
+  end.
+
+Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t.
+
+Ltac revert_last := 
+  match goal with
+    [ H : _ |- _ ] => revert H
+  end.
+
+Ltac reverse := repeat revert_last.
 
 Ltac on_call f tac :=
   match goal with
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index bf4876a03..67bd70baf 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -10,7 +10,7 @@ Notation "{ ( x , y )  :  A  |  P }" :=
 
 Notation " ! " := (False_rect _ _).
 
-Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
+Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
 Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
 
 (** Coerces objects before comparing them *)
@@ -29,7 +29,7 @@ Require Import Coq.Bool.Sumbool.
 Notation "'dec'" := (sumbool_of_bool) (at level 0). 
 
 (** Default simplification tactic. *)
-Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; 
+Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
   try (solve [ red ; intros ; discriminate ]) ; auto with *.  
 
 (** Extraction directives *)
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index b15dd97b1..7295fd24d 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -373,9 +373,10 @@ let admit_obligations n =
     Array.mapi (fun i x -> 
 		 match x.obl_body with 
 		     None -> 
-			 let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
-			   assumption_message x.obl_name;
-			   { x with obl_body = Some (mkConst kn) }
+                       let x = subst_deps_obl obls x in
+		       let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+			 assumption_message x.obl_name;
+			 { x with obl_body = Some (mkConst kn) }
 		   | Some _ -> x)
       obls
   in