diff options
Diffstat (limited to 'tactics/tacinterp.mli')
-rw-r--r-- | tactics/tacinterp.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 6b7aabe2e..18873d1c6 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -27,7 +27,7 @@ open Redexpr (* Values for interpretation *) type value = | VRTactic of (goal list sigma * validation) - | VFun of ltac_trace * (identifier*value) list * + | VFun of ltac_trace * (identifier*value) list * identifier option list * glob_tactic_expr | VVoid | VInteger of int @@ -44,7 +44,7 @@ and interp_sign = debug : debug_info; trace : ltac_trace } -val extract_ltac_vars : interp_sign -> Evd.evar_defs -> Environ.env -> +val extract_ltac_vars : interp_sign -> Evd.evar_defs -> Environ.env -> Pretyping.var_map * Pretyping.unbound_ltac_var_map (* Transforms an id into a constr if possible *) @@ -53,7 +53,7 @@ val constr_of_id : Environ.env -> identifier -> constr (* 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 @@ -88,7 +88,7 @@ type glob_sign = { val add_interp_genarg : string -> (glob_sign -> raw_generic_argument -> glob_generic_argument) * - (interp_sign -> goal sigma -> glob_generic_argument -> + (interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument) * (substitution -> glob_generic_argument -> glob_generic_argument) -> unit @@ -99,14 +99,14 @@ val interp_genarg : val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument -val intern_tactic : +val intern_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr val intern_constr : glob_sign -> constr_expr -> rawconstr_and_expr val intern_constr_with_bindings : - glob_sign -> constr_expr * constr_expr Rawterm.bindings -> + glob_sign -> constr_expr * constr_expr Rawterm.bindings -> rawconstr_and_expr * rawconstr_and_expr Rawterm.bindings val intern_hyp : @@ -122,7 +122,7 @@ val subst_rawconstr_and_expr : val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value (* Interprets an expression that evaluates to a constr *) -val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> +val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> constr (* Interprets redexp arguments *) @@ -134,7 +134,7 @@ val interp_tac_gen : (identifier * value) list -> identifier list -> val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier -val interp_bindings : interp_sign -> goal sigma -> rawconstr_and_expr Rawterm.bindings -> +val interp_bindings : interp_sign -> goal sigma -> rawconstr_and_expr Rawterm.bindings -> Evd.open_constr Rawterm.bindings (* Initial call for interpretation *) @@ -158,7 +158,7 @@ val hide_interp : raw_tactic_expr -> tactic option -> tactic val declare_implicit_tactic : tactic -> unit (* Declare the xml printer *) -val declare_xml_printer : +val declare_xml_printer : (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit (* printing *) |