diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 71 |
1 files changed, 31 insertions, 40 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 8f585781..d9dc8094 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacinterp.mli 14677 2011-11-17 22:19:38Z herbelin $ i*) - -(*i*) open Pp open Util open Names @@ -21,11 +18,10 @@ open Genarg open Topconstr open Mod_subst open Redexpr -(*i*) -(* Values for interpretation *) +(** Values for interpretation *) type value = - | VRTactic of (goal list sigma * validation) + | VRTactic of (goal list sigma) | VFun of ltac_trace * (identifier*value) list * identifier option list * glob_tactic_expr | VVoid @@ -36,7 +32,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,31 +42,27 @@ and interp_sign = val extract_ltac_constr_values : interp_sign -> Environ.env -> Pretyping.ltac_var_map -(* 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) val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr 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 +70,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; @@ -99,18 +91,15 @@ val interp_genarg : val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument -val intern_tactic : - glob_sign -> raw_tactic_expr -> glob_tactic_expr - val intern_pure_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr val intern_constr : - glob_sign -> constr_expr -> rawconstr_and_expr + glob_sign -> constr_expr -> glob_constr_and_expr val intern_constr_with_bindings : - glob_sign -> constr_expr * constr_expr Rawterm.bindings -> - rawconstr_and_expr * rawconstr_and_expr Rawterm.bindings + glob_sign -> constr_expr * constr_expr Glob_term.bindings -> + glob_constr_and_expr * glob_constr_and_expr Glob_term.bindings val intern_hyp : glob_sign -> identifier Util.located -> identifier Util.located @@ -118,28 +107,34 @@ val intern_hyp : val subst_genarg : substitution -> glob_generic_argument -> glob_generic_argument -val subst_rawconstr_and_expr : - substitution -> rawconstr_and_expr -> rawconstr_and_expr +val subst_glob_constr_and_expr : + substitution -> glob_constr_and_expr -> glob_constr_and_expr -(* Interprets any expression *) +val subst_glob_with_bindings : + substitution -> glob_constr_and_expr Glob_term.with_bindings -> glob_constr_and_expr Glob_term.with_bindings + +(** 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 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 +val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.bindings -> Evd.evar_map * constr Glob_term.bindings + +val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr Glob_term.with_bindings -> Evd.evar_map * constr Glob_term.with_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 @@ -152,21 +147,18 @@ 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 *) -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 @@ -175,4 +167,3 @@ val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> iden val interp_int : interp_sign -> identifier located -> int val error_ltac_variable : loc -> identifier -> Environ.env option -> value -> string -> 'a - |