diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /tactics/tacinterp.mli | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'tactics/tacinterp.mli')
-rw-r--r-- | tactics/tacinterp.mli | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index d9dc8094..b9fd64f6 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -77,16 +77,18 @@ type glob_sign = { gsigma : Evd.evar_map; genv : Environ.env } +val fully_empty_glob_sign : glob_sign + val add_interp_genarg : string -> (glob_sign -> raw_generic_argument -> glob_generic_argument) * (interp_sign -> goal sigma -> glob_generic_argument -> - typed_generic_argument) * + Evd.evar_map * typed_generic_argument) * (substitution -> glob_generic_argument -> glob_generic_argument) -> unit val interp_genarg : - interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument + interp_sign -> goal sigma -> glob_generic_argument -> Evd.evar_map * typed_generic_argument val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument @@ -114,14 +116,14 @@ 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 +val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value (** Interprets an expression that evaluates to a constr *) val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> - constr + Evd.evar_map * constr (** Interprets redexp arguments *) -val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr +val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr (** Interprets tactic expressions *) val interp_tac_gen : (identifier * value) list -> identifier list -> @@ -143,7 +145,7 @@ val eval_tactic : glob_tactic_expr -> tactic val interp : raw_tactic_expr -> tactic -val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr +val eval_ltac_constr : goal sigma -> raw_tactic_expr -> Evd.evar_map * constr val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr |