From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- proofs/pfedit.mli | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index edbc18a3..5e0fb4dd 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -157,6 +157,14 @@ val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context +val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic -> + constr * Evd.evar_map +(** A variant of the above function that handles open terms as well. + Caveat: all effects are purged in the returned term at the end, but other + evars solved by side-effects are NOT purged, so that unexpected failures may + occur. Ideally all code using this function should be rewritten in the + monad. *) + (** Declare the default tactic to fill implicit arguments *) val declare_implicit_tactic : unit Proofview.tactic -> unit -- cgit v1.2.3