diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 54 |
1 files changed, 26 insertions, 28 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 71ee29f8c..771d28fba 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* 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 Pp open Util open Names @@ -21,9 +20,8 @@ open Genarg open Topconstr open Mod_subst open Redexpr -(*i*) -(* Values for interpretation *) +(** Values for interpretation *) type value = | VRTactic of (goal list sigma) | VFun of ltac_trace * (identifier*value) list * @@ -36,7 +34,7 @@ type value = | VList of value list | VRec of (identifier*value) list ref * glob_tactic_expr -(* Signature for interpretation: val\_interp and interpretation functions *) +(** Signature for interpretation: val\_interp and interpretation functions *) and interp_sign = { lfun : (identifier * value) list; avoid_ids : identifier list; @@ -46,10 +44,10 @@ and interp_sign = val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> Pretyping.var_map * Pretyping.unbound_ltac_var_map -(* Transforms an id into a constr if possible *) +(** Transforms an id into a constr if possible *) val constr_of_id : Environ.env -> identifier -> constr -(* To embed several objects in Coqast.t *) +(** To embed several objects in Coqast.t *) val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr) @@ -58,19 +56,19 @@ val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr val valueIn : value -> raw_tactic_arg val constrIn : constr -> constr_expr -(* Sets the debugger mode *) +(** Sets the debugger mode *) val set_debug : debug_info -> unit -(* Gives the state of debug *) +(** Gives the state of debug *) val get_debug : unit -> debug_info -(* Adds a definition for tactics in the table *) +(** Adds a definition for tactics in the table *) val add_tacdef : Vernacexpr.locality_flag -> bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit -(* Tactic extensions *) +(** Tactic extensions *) val add_tactic : string -> (typed_generic_argument list -> tactic) -> unit val overwriting_add_tactic : @@ -78,7 +76,7 @@ val overwriting_add_tactic : val lookup_tactic : string -> (typed_generic_argument list) -> tactic -(* Adds an interpretation function for extra generic arguments *) +(** Adds an interpretation function for extra generic arguments *) type glob_sign = { ltacvars : identifier list * identifier list; ltacrecvars : (identifier * Nametab.ltac_constant) list; @@ -118,17 +116,17 @@ val subst_genarg : val subst_rawconstr_and_expr : substitution -> rawconstr_and_expr -> rawconstr_and_expr -(* Interprets any expression *) +(** Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value -(* Interprets an expression that evaluates to a constr *) +(** Interprets an expression that evaluates to a constr *) val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> constr -(* Interprets redexp arguments *) +(** Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr -(* Interprets tactic expressions *) +(** Interprets tactic expressions *) val interp_tac_gen : (identifier * value) list -> identifier list -> debug_info -> raw_tactic_expr -> tactic @@ -136,7 +134,7 @@ val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> rawconstr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings -(* Initial call for interpretation *) +(** Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr @@ -149,21 +147,21 @@ val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr -(* Hides interpretation for pretty-print *) +(** Hides interpretation for pretty-print *) val hide_interp : raw_tactic_expr -> tactic option -> tactic -(* Declare the default tactic to fill implicit arguments *) +(** Declare the default tactic to fill implicit arguments *) val declare_implicit_tactic : tactic -> unit -(* Declare the xml printer *) +(** Declare the xml printer *) val declare_xml_printer : (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit -(* printing *) +(** printing *) val print_ltac : Libnames.qualid -> std_ppcmds -(* Internals that can be useful for syntax extensions. *) +(** Internals that can be useful for syntax extensions. *) exception CannotCoerceTo of string |