Add [Next Obligation with tactic] support (wish #1953).

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

3 files changed, 30 insertions, 23 deletions

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 6d4eaabed..113b16800 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -41,7 +41,7 @@ struct
 		(* types *)
   let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
 
-  let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt"
+  let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.Entry.e = gec "subtac_withtac"
 end
 
 open Rawterm
@@ -53,17 +53,17 @@ open Constr
 let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 GEXTEND Gram
-  GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt;
+  GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_withtac;
 
   subtac_gallina_loc:
     [ [ g = Vernac.gallina -> loc, g
     | g = Vernac.gallina_ext -> loc, g ] ]
     ;
 
-  subtac_nameopt:
-    [ [ "ofb"; id=Prim.ident -> Some (id)
+  subtac_withtac:
+    [ [ "with"; t = Tactic.tactic -> Some t
       | -> None ] ]
-    ;
+  ;
 
   Constr.binder_let:
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
@@ -90,12 +90,12 @@ let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
   (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) =
   Genarg.create_arg "subtac_gallina_loc"
 
-type 'a nameopt_argtype = (identifier option, 'a) Genarg.abstract_argument_type
+type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
 
-let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype),
-  (globwit_subtac_nameopt : Genarg.glevel nameopt_argtype),
-  (rawwit_subtac_nameopt : Genarg.rlevel nameopt_argtype) =
-  Genarg.create_arg "subtac_nameopt"
+let (wit_subtac_withtac : Genarg.tlevel withtac_argtype),
+  (globwit_subtac_withtac : Genarg.glevel withtac_argtype),
+  (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) =
+  Genarg.create_arg "subtac_withtac"
 
 VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
@@ -113,12 +113,17 @@ let solve_all_obligations e = try_catch_exn Subtac_obligations.solve_all_obligat
 let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e
 
 VERNAC COMMAND EXTEND Subtac_Obligations
-| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ subtac_obligation (num, Some name, Some t) ]
-| [ "Obligation" integer(num) "of" ident(name) ] -> [ subtac_obligation (num, Some name, None) ]
-| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ subtac_obligation (num, None, Some t) ]
-| [ "Obligation" integer(num) ] -> [ subtac_obligation (num, None, None) ]
-| [ "Next" "Obligation" "of" ident(name) ] -> [ next_obligation (Some name) ]
-| [ "Next" "Obligation" ] -> [ next_obligation None ]
+| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) subtac_withtac(tac) ] -> 
+    [ subtac_obligation (num, Some name, Some t) tac ]
+| [ "Obligation" integer(num) "of" ident(name) subtac_withtac(tac) ] -> 
+    [ subtac_obligation (num, Some name, None) tac ]
+| [ "Obligation" integer(num) ":" lconstr(t) subtac_withtac(tac) ] -> 
+    [ subtac_obligation (num, None, Some t) tac ]
+| [ "Obligation" integer(num) subtac_withtac(tac) ] -> 
+    [ subtac_obligation (num, None, None) tac ]
+| [ "Next" "Obligation" "of" ident(name) subtac_withtac(tac) ] -> 
+    [ next_obligation (Some name) tac ]
+| [ "Next" "Obligation" subtac_withtac(tac) ] -> [ next_obligation None tac ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligation
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 5766c0641..5f7114ba5 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -428,7 +428,7 @@ let not_transp_msg =
 let warn_not_transp () = ppwarn not_transp_msg
 let error_not_transp () = pperror not_transp_msg
 
-let rec solve_obligation prg num =
+let rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
@@ -470,18 +470,19 @@ let rec solve_obligation prg num =
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
 	    Pfedit.by !default_tactic;
+	    Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac;
 	    Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
       | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 		       ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
 
-and subtac_obligation (user_num, name, typ) =
+and subtac_obligation (user_num, name, typ) tac =
   let num = pred user_num in
   let prg = get_prog_err name in
   let obls, rem = prg.prg_obligations in
     if num < Array.length obls then
       let obl = obls.(num) in
 	match obl.obl_body with
-	    None -> solve_obligation prg num
+	    None -> solve_obligation prg num tac
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
 
@@ -639,13 +640,13 @@ let array_find f arr =
     raise Not_found
   with Found i -> i
 
-let next_obligation n =
+let next_obligation n tac =
   let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
   let i =
     try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
     with Not_found -> anomaly "Could not find a solvable obligation."
-  in solve_obligation prg i
+  in solve_obligation prg i tac
 
 let default_tactic () = !default_tactic
 let default_tactic_expr () = !default_tactic_expr
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 5b7a4f7d0..df7cd684a 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -43,9 +43,10 @@ val add_mutual_definitions :
   notations ->
   fixpoint_kind -> unit
 
-val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
+val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option ->
+  Tacexpr.raw_tactic_expr option -> unit
 
-val next_obligation : Names.identifier option -> unit
+val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit
 
 val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)