aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacinterp.mli')
-rw-r--r--tactics/tacinterp.mli18
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 *)