diff options
Diffstat (limited to 'toplevel/vernacentries.mli')
| -rw-r--r-- | toplevel/vernacentries.mli | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 58df8a906..fa9f2b7c2 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,34 +1,33 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Term open Vernacinterp open Vernacexpr open Topconstr -(*i*) -(* Vernacular entries *) +(** 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 +(** 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 *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env (*i -(* this function is used to analyse the extra arguments in search commands. + +(** this function is used to analyse the extra arguments in search commands. It is used in pcoq. *) (*i anciennement: inside_outside i*) val interp_search_restriction : search_restriction -> dir_path list * bool i*) @@ -47,7 +46,7 @@ type pcoq_hook = { val set_pcoq_hook : pcoq_hook -> unit -(* This function makes sure that the function given in argument is preceded +(** This function makes sure that the function given in argument is preceded by a command aborting all proofs if necessary. It is used in pcoq. *) val abort_refine : ('a -> unit) -> 'a -> unit;; |