Better solve using tactics impl.

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

2 files changed, 30 insertions, 6 deletions

diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index e2192f28d0..de362da889 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -300,11 +300,14 @@ let solve_obligations n tac =
 		 match x.obl_body with 
 		     Some _ -> x
 		   | None -> 
-		       try
-			 let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
-			   decr rem;
-			   { x with obl_body = Some t }
-		       with _ -> x)
+		       (try
+			  let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
+			    decr rem;
+			    { x with obl_body = Some t }
+			with UserError (s, cmds) ->
+			  debug 1 cmds;
+			  x
+			  | _ -> x))
       obls
   in
     update_obls prg obls' !rem
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 8164910f29..3279ad4c51 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -578,14 +578,35 @@ let recursive_message v =
 		    spc () ++ str "are recursively defined")
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
+(*
 let solve_by_tac ev t =
   debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev);
   let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in
+  debug 1 (str "Goal created");
   let ts = Tacmach.mk_pftreestate goal in
+  debug 1 (str "Got pftreestate");
   let solved_state = Tacmach.solve_pftreestate t ts in
-  let c = Tacmach.extract_pftreestate solved_state in
+  debug 1 (str "Solved goal");
+    let _, l = Tacmach.extract_open_pftreestate solved_state in
+      List.iter (fun (_, x) -> debug 1 (str "left hole of type " ++ my_print_constr (Global.env()) x)) l;
+    let c = Tacmach.extract_pftreestate solved_state in
+    debug 1 (str "Extracted term");
     debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
     c
+    *)
+
+let solve_by_tac evi t =
+  debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
+  let id = id_of_string "H" in
+  Pfedit.start_proof id (Decl_kinds.Local,Decl_kinds.Proof Decl_kinds.Lemma) evi.evar_hyps evi.evar_concl
+    (fun _ _ -> ());
+  try
+    Pfedit.by (tclCOMPLETE t);
+    let _,(const,_,_) = Pfedit.cook_proof () in 
+      Pfedit.delete_current_proof (); const.Entries.const_entry_body
+  with e when Logic.catchable_exception e -> 
+    Pfedit.delete_current_proof();
+    raise Exit
 
 let rec string_of_list sep f = function
     [] -> ""