Add Solve All Obligations command, fix bug in inequality generation introduced by previous commit, add general purpose tactics for destructing existentials and disjunctions. Compiles without camlp4 warnings too.

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

6 files changed, 43 insertions, 6 deletions

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index d1e3caf7d..d38902c96 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -40,6 +40,19 @@ Ltac destruct_one_ex :=
 
 Ltac destruct_exists := repeat (destruct_one_ex).
 
+Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
+
+Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
+
+Tactic Notation "contradiction" "by" constr(t) := 
+  let H := fresh in assert t as H by auto with * ; contradiction.
+
+Ltac discriminates :=
+  match goal with
+    | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity
+    | _ => discriminate
+  end.
+
 Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
 
 Ltac on_last_hyp tac := 
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 137ac8c98..a83a321de 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -25,9 +25,14 @@ Notation "'forall' { x : A | P } , Q" :=
   (forall x:{x:A|P}, Q)
   (at level 200, x ident, right associativity).
 
-Require Import Coq.Bool.Sumbool.	
+Require Import Coq.Bool.Sumbool.
+(** Construct a dependent disjunction from a boolean. *)
 Notation "'dec'" := (sumbool_of_bool) (at level 0). 
 
+(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
+Notation in_right := (@right _ _ _).
+Notation in_left := (@left _ _ _).
+
 (** Default simplification tactic. *)
 Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
   try (solve [ red ; intros ; discriminate ]) ; auto with *.  
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 9e9a76707..05334ad76 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -111,6 +111,16 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations
     [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ]
 | [ "Solve" "Obligations" ] -> 
     [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ]
+      END
+
+VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
+| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> 
+    [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ]
+| [ "Solve" "All" "Obligations" ] -> 
+    [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ]
+      END
+
+VERNAC COMMAND EXTEND Subtac_Admit_Obligations
 | [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] 
 | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] 
     END
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index cbfff99e8..7f71bfa72 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1755,8 +1755,8 @@ let build_ineqs prevpatterns pats liftsign =
 			  succ n, (* nth pattern *)
 			  mkApp (Lazy.force eq_ind,
 				[| lift (lens + liftsign) ppat_ty ;
-				   ppat_c ; 
-				   (*liftn liftsign lens ppat_c ; *)
+(* 				   ppat_c ;  *)
+				   liftn liftsign (succ lens) ppat_c ;
 				   lift len' curpat_c |]) :: 
 			    List.map 
 			    (fun t -> 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d19e86786..3c8fd1d45 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -352,8 +352,7 @@ and solve_obligation_by_tac prg obls i tac =
 	   else false
 	 with _ -> false)  
 
-and solve_obligations n tac = 
-  let prg = get_prog n in
+and solve_prg_obligations prg tac = 
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
   let obls' = Array.copy obls in
@@ -364,6 +363,13 @@ and solve_obligations n tac =
       obls'
   in
     update_obls prg obls' !rem
+
+and solve_obligations n tac = 
+  let prg = get_prog n in
+    solve_prg_obligations prg tac
+
+and solve_all_obligations tac = 
+  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
       
 and try_solve_obligations n tac = 
   ignore (solve_obligations n tac)
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 0ad9e730d..8a6455136 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -17,7 +17,10 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 val next_obligation : Names.identifier option -> unit
 
 val solve_obligations : Names.identifier option -> Proof_type.tactic -> int 
-  (* Number of remaining obligations to be solved for this program *)
+(* Number of remaining obligations to be solved for this program *)
+
+val solve_all_obligations : Proof_type.tactic -> unit 
+
 val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
 val show_obligations : Names.identifier option -> unit