diff options
Diffstat (limited to 'toplevel/vernacentries.mli')
| -rw-r--r-- | toplevel/vernacentries.mli | 39 |
1 files changed, 14 insertions, 25 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 9a400fe6..4b1cd7a0 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,52 +1,36 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Term -open Vernacinterp -open Vernacexpr -open Topconstr +open Misctypes -val dump_global : Libnames.reference Genarg.or_by_notation -> unit +val dump_global : Libnames.reference or_by_notation -> unit (** Vernacular entries *) -val show_script : unit -> unit val show_prooftree : unit -> unit val show_node : unit -> unit (** This function can be used by any command that want to observe terms - in the context of the current goal, as for instance in pcoq *) + in the context of the current goal *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env -type pcoq_hook = { - start_proof : unit -> unit; - solve : int -> unit; - abort : string -> unit; - search : searchable -> dir_path list * bool -> unit; - print_name : Libnames.reference Genarg.or_by_notation -> unit; - print_check : Environ.env -> Environ.unsafe_judgment -> unit; - print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> - Environ.unsafe_judgment -> unit; - show_goal : goal_reference -> unit -} - -val set_pcoq_hook : pcoq_hook -> unit - (** The main interpretation function of vernacular expressions *) - -val interp : Vernacexpr.vernac_expr -> unit +val interp : + ?verbosely:bool -> + ?proof:Proof_global.closed_proof -> + Loc.t * Vernacexpr.vernac_expr -> unit (** Print subgoals when the verbose flag is on. Meant to be used inside vernac commands from plugins. *) val print_subgoals : unit -> unit +val try_print_subgoals : unit -> unit (** The printing of goals via [print_subgoals] or during [interp] can be controlled by the following flag. @@ -67,3 +51,8 @@ val qed_display_script : bool ref a known inductive type. *) val make_cases : string -> string list list + +val vernac_end_proof : + ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit + +val with_fail : bool -> (unit -> unit) -> unit |