diff options
Diffstat (limited to 'toplevel/vernacentries.mli')
-rw-r--r-- | toplevel/vernacentries.mli | 66 |
1 files changed, 0 insertions, 66 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli deleted file mode 100644 index 4e7fa4a0..00000000 --- a/toplevel/vernacentries.mli +++ /dev/null @@ -1,66 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Misctypes - -val dump_global : Libnames.reference or_by_notation -> unit - -(** Vernacular entries *) - -val show_prooftree : unit -> unit - -val show_node : unit -> unit - -val vernac_require : - Libnames.reference option -> bool option -> Libnames.reference list -> unit - -(** This function can be used by any command that want to observe terms - in the context of the current goal *) -val get_current_context_of_args : int option -> Evd.evar_map * Environ.env - -(** The main interpretation function of vernacular expressions *) -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. - Used for instance by coqide, since it has its own - goal-fetching mechanism. *) - -val enable_goal_printing : bool ref - -(** Should Qed try to display the proof script ? - True by default, but false in ProofGeneral and coqIDE *) - -val qed_display_script : bool ref - -(** Prepare a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. - [Not_found] is raised if the given string isn't the qualid of - 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 - -val command_focus : unit Proof.focus_kind - -val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr -> - Evd.evar_map * Redexpr.red_expr) Hook.t |