Some usability enhancements.

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

4 files changed, 27 insertions, 17 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 1ec77c6903..3d9c763815 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -37,6 +37,7 @@ struct
   let gec s = Gram.Entry.create ("Subtac."^s)
 		(* types *)
   let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
+
 end
 
 open SubtacGram 
@@ -63,6 +64,8 @@ GEXTEND Gram
 	  let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in
 	    ([id], typ) ] ];
 
+
+
   END
 
 
@@ -75,8 +78,10 @@ let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_arg
 
 VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
-| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name) ]
-| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None) ]      
+| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ]
+| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ]
+| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ]      
+| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ]      
 | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
 | [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
 | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index de362da889..7a1c403232 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -174,16 +174,19 @@ let try_tactics obls =
 	 | _ -> obl)
     obls
         
+let red = Reductionops.nf_betaiota
 
 let init_prog_info n b t deps obls =
   let obls' = 
     Array.mapi
       (fun i (n, t, d) ->
 	 debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
-         { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d })
+         { obl_name = n ; obl_body = None; 
+	   obl_type = red t; 
+	   obl_deps = d })
       obls
   in
-    { prg_name = n ; prg_body = b; prg_type = t; prg_obligations = (obls', Array.length obls');
+    { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
       prg_deps = deps }
     
 let pperror cmd = Util.errorlabstrm "Subtac" cmd
@@ -192,7 +195,9 @@ let error s = pperror (str s)
 let get_prog name =
   let prg_infos = !from_prg in
     match name with
-	Some n -> ProgMap.find n prg_infos
+	Some n -> 
+	  (try ProgMap.find n prg_infos
+	   with Not_found -> error ("No obligations for program " ^ string_of_id n))
       | None -> 
 	  (let n = map_cardinal prg_infos in
 	     match n with 
@@ -254,7 +259,7 @@ let deps_remaining obls x =
 	 else x :: acc)
       deps []
 
-let subtac_obligation (user_num, name) =
+let subtac_obligation (user_num, name, typ) =
   let num = pred user_num in
   let prg = get_prog name in
   let obls, rem = prg.prg_obligations in
@@ -315,12 +320,13 @@ let solve_obligations n tac =
 open Pp
 let show_obligations n =
   let prg = get_prog n in
+  let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
     msgnl (int rem ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x -> 
 		   match x.obl_body with 
-		       None -> msgnl (int (succ i) ++ str " : " ++ spc () ++ 
-					my_print_constr (Global.env ()) x.obl_type)
+		       None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
+					my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
 		    | Some _ -> ())
       obls
 			
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 6ba479764f..07f151697a 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -8,7 +8,7 @@ val add_definition : Names.identifier ->  Term.constr -> Term.types ->
 val add_mutual_definitions : 
   (Names.identifier * int * Term.constr * Term.types * obligation_info) list -> unit
 
-val subtac_obligation : int * Names.identifier option -> unit
+val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
 
 val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 7fa80fbd0c..39fdc9ba75 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -9,20 +9,19 @@ Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
   (S q' & r)
   else (O & a).
 
-Obligations.
-
 Require Import Coq.subtac.Utils.
 Require Import Coq.subtac.FixSub.
 Require Import Omega.
+Obligations.
 
 Obligation 1.
-  simpl ; intros.
+  intros.
   destruct_exists ; simpl in * ; auto with arith.
   omega.
 Qed.
 
 Obligation 2 of euclid.
-  simpl ; intros.
+  intros.
   destruct_exists ; simpl in * ; auto with arith.
   assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
 Qed.
@@ -32,7 +31,7 @@ Obligation 4 of euclid.
 Qed.
 
 Obligation 3 of euclid.
-  simpl ; intros.
+  intros.
   destruct_exists ; simpl in *.
   omega.
 Qed.
@@ -44,10 +43,10 @@ Extraction le_lt_dec.
 Extraction euclid.
 
 
-Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
-  (a & a).
+Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } :=
+  (a & S a).
 
 
-Solve Obligations using simpl ; auto.
+Solve Obligations using auto with zarith.
 
 Extraction testsig.