diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 68f6f6ac..7c0180a6 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacinterp.mli 7841 2006-01-11 11:24:54Z herbelin $ i*) +(*i $Id: tacinterp.mli 8975 2006-06-23 08:52:53Z herbelin $ i*) (*i*) open Dyn open Pp +open Util open Names open Proof_type open Tacmach @@ -20,6 +21,7 @@ open Tacexpr open Genarg open Topconstr open Mod_subst +open Redexpr (*i*) (* Values for interpretation *) @@ -39,12 +41,6 @@ and interp_sign = { lfun : (identifier * value) list; debug : debug_info } -(* Gives the identifier corresponding to an Identifier [tactic_arg] *) -val id_of_Identifier : Environ.env -> value -> identifier - -(* Gives the constr corresponding to a Constr [value] *) -val constr_of_VConstr : Environ.env -> value -> constr - (* Transforms an id into a constr if possible *) val constr_of_id : Environ.env -> identifier -> constr @@ -103,16 +99,18 @@ val subst_rawconstr_and_expr : (* Interprets any expression *) 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 -> + constr + (* Interprets redexp arguments *) -val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr - -> Redexpr.red_expr +val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr (* Interprets tactic expressions *) val interp_tac_gen : (identifier * value) list -> debug_info -> raw_tactic_expr -> tactic -val interp_hyp : interp_sign -> goal sigma -> - identifier Util.located -> identifier +val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier (* Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr @@ -123,6 +121,8 @@ val eval_tactic : glob_tactic_expr -> tactic val interp : raw_tactic_expr -> tactic +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 *) |