Update some tests and fix section bug.

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

5 files changed, 98 insertions, 101 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 412d5ae3b..34d9f6206 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -6,6 +6,8 @@ Notation "'fun' { x : A | P } => Q" :=
 
 Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
 
+Notation " ! " := (False_rect _ _).
+
 Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
 intros.
 induction t.
@@ -44,7 +46,7 @@ end.
 
 Ltac destruct_exists := repeat (destruct_one_pair) .
 
-Ltac subtac_simpl := hnf ; intros ; destruct_exists ; try subst.
+Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto. 
 
 (* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
 Ltac destruct_call f :=
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 5119145f4..4a1719528 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -39,7 +39,7 @@ let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
 
 let set_default_tactic t = default_tactic := t
 
-let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; 
+let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
 			     evar_concl = o.obl_type ; 
 			     evar_body = Evar_empty ;
 			     evar_extra = None }
@@ -221,7 +221,7 @@ let update_obls prg obls rem =
       Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining");
     )
     else (
-      debug 2 (str "No more obligations remaining");
+      Options.if_verbose msgnl (str "No more obligations remaining");
       match prg'.prg_deps with
 	  [] ->
 	    declare_definition prg';
@@ -259,9 +259,9 @@ let solve_obligation prg num =
 		   let obls = Array.copy obls in
 		   let _ = obls.(num) <- obl in
 		     update_obls prg obls (pred rem));
-	      Pfedit.by !default_tactic;
 	      trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
-		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type)
+		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
+	      Pfedit.by !default_tactic
 	| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 			++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 973d2a150..d60ee0084 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -616,12 +616,15 @@ let solve_by_tac ev t =
     c
     *)
 
+let ($) f g = fun x -> f (g x)
+
 let solve_by_tac evi t =
   debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
   let id = id_of_string "H" in
   try 
-    Pfedit.start_proof id (Decl_kinds.Local,Decl_kinds.Proof Decl_kinds.Lemma) evi.evar_hyps evi.evar_concl
+    Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
     (fun _ _ -> ());
+    debug 2 (str "Started proof");
     Pfedit.by (tclCOMPLETE t);
     let _,(const,_,_) = Pfedit.cook_proof () in 
       Pfedit.delete_current_proof (); const.Entries.const_entry_body
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 8429c2670..fb8b34eed 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,95 +1,82 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import Coq.subtac.Utils.
 Require Import List.
 
-Variable A : Set.
-
-Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
-  fun l =>
-    match `l with
-    | nil => _
-    | hd :: tl => hd
-    end.
-Proof.
-  destruct l ; simpl ; intro H.
-  rewrite H in n ; intuition.
-Defined.
+Set Implicit Arguments.
 
+Section Accessors.
+  Variable A : Set.
 
-Extraction myhd.
-Extraction Inline proj1_sig.
+  Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
+    fun l =>
+      match l with
+        | nil => !
+        | hd :: tl => hd
+      end.
 
-Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
-  fun l => 
+  Program Definition mytail (l : list A | length l <> 0) : list A :=
     match l with
-    | nil => _
-    | hd :: tl => tl
+      | nil => !
+      | hd :: tl => tl
     end.
-Proof.
-destruct l ; simpl ; intro H ; rewrite H in n ; intuition.
-Defined.
-
-Extraction mytail.
-
-Variable a : A.
-
-Program Definition test_hd : A := myhd (cons a nil).
-Proof.
-simpl ; auto.
-Defined.
+End Accessors.
 
-Extraction test_hd.
+Program Definition test_hd : nat := myhd (cons 1 nil).
 
+(*Eval compute in test_hd*)
 (*Program Definition test_tail : list A := mytail nil.*)
 
+Section app.
+  Variable A : Set.
 
+  Program Fixpoint app (l : list A) (l' : list A) { struct l } :
+    { r : list A | length r = length l + length l' } :=
+    match l with
+      | nil => l'
+      | hd :: tl => hd :: (tl ++ l')
+    end 
+    where "x ++ y" := (app x y).
+ 
+  Next Obligation.
+    intros.
+    destruct_call app ; subtac_simpl.
+  Defined.
+  
+  Program Lemma app_id_l : forall l : list A, l = nil ++ l.
+  Proof.
+    simpl ; auto.
+  Qed.
+  
+  Program Lemma app_id_r : forall l : list A, l = l ++ nil.
+  Proof.
+    induction l ; simpl ; auto.
+    rewrite <- IHl ; auto.
+  Qed.
+
+End app.
+
+Extraction app.
+
+Section Nth.
+
+  Variable A : Set.
+
+  Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := 
+    match n, l with
+      | 0, hd :: _ => hd
+      | S n', _ :: tl => nth tl n'
+      | _, nil => !
+    end.
 
-
-
-Program Fixpoint append (l : list A) (l' : list A) { struct l } :
- { r : list A | length r = length l + length l' } :=
- match l with
- | nil => l'
- | hd :: tl => hd :: (append tl l')
- end.
-subst ; auto.
-simpl ; rewrite (subset_simpl (append tl0 l')).
-simpl ; subst.
-simpl ; auto.
-Defined.
-
-Extraction append.
-
-
-Program Lemma append_app' : forall l : list A, l = append nil l.
-Proof.
-simpl ; auto.
-Qed.
-
-Program Lemma append_app : forall l : list A, l = append l nil.
-Proof.
-intros.
-induction l ; simpl ; auto.
-simpl in IHl.
-rewrite <- IHl.
-reflexivity.
-Qed.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+  Next Obligation.
+  Proof.
+    intros.
+    simpl in * ; auto with arith.
+  Defined.
+
+  Next Obligation.
+  Proof.
+    intros.
+    inversion l0.
+  Defined.
+End Nth.
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index f73507d2f..87ab47d63 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,33 +1,38 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import JMeq.
 Require Import List.
 Require Import Coq.subtac.Utils.
 
+Set Implicit Arguments.
+
 Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
   | 0 => nil
   | S p => 
     match l with
-    | cons hd tl => let rest := take A tl p in cons hd rest
-    | nil => _
+    | cons hd tl => let rest := take tl p in cons hd rest
+    | nil => !
     end
   end.
 
 Require Import Omega.
 
-Obligations.
-
-Solve Obligations using (subtac_simpl ; subst ; auto with arith).
-
-Obligations.
+Next Obligation.
+  intros.
+  simpl in l0.
+  apply le_S_n ; exact l0.
+Defined.
 
-Obligation 3.
-  destruct_call take ; subtac_simpl ; subst ; auto.
+Next Obligation.
+  intros.
+  destruct_call take ; subtac_simpl.
 Defined.
 
-Obligation 4.
-  subst l x.
-  simpl in l0.
-  absurd (S p <= 0) ; omega.
+Next Obligation.
+  intros.
+  inversion l0.
 Defined.
 
-Extraction take.
+
+
+