diff options
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 13 | ||||
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 23 |
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 [] -> "" |