diff options
Diffstat (limited to 'interp/constrarg.mli')
| -rw-r--r-- | interp/constrarg.mli | 43 |
1 files changed, 27 insertions, 16 deletions
diff --git a/interp/constrarg.mli b/interp/constrarg.mli index ebef1ada..6ccd944d 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -26,7 +26,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t (** {5 Additional generic arguments} *) -val wit_int_or_var : int or_var uniform_genarg_type +val wit_int_or_var : (int or_var, int or_var, int) genarg_type val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type @@ -38,39 +38,50 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type - -val wit_sort : (glob_sort, glob_sort, sorts) genarg_type - val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_constr_may_eval : - ((constr_expr,reference or_by_notation,constr_expr) may_eval, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval, - constr) genarg_type - val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : - (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type + (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_constr_with_bindings : (constr_expr with_bindings, glob_constr_and_expr with_bindings, - constr with_bindings Evd.sigma) genarg_type + constr with_bindings delayed_open) genarg_type val wit_bindings : (constr_expr bindings, glob_constr_and_expr bindings, - constr bindings Evd.sigma) genarg_type - -val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type + constr bindings delayed_open) genarg_type val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type +val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type + +(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their + toplevel interpretation. The one of [wit_ltac] forces the tactic and + discards the result. *) +val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type + +val wit_destruction_arg : + (constr_expr with_bindings destruction_arg, + glob_constr_and_expr with_bindings destruction_arg, + delayed_open_constr_with_bindings destruction_arg) genarg_type + +(** Aliases for compatibility *) + +val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type +val wit_global : (reference, global_reference located or_var, global_reference) genarg_type +val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type +val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_redexpr : + ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type |