diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.ml')
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |