diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 10 | ||||
| -rw-r--r-- | interp/constrarg.mli | 12 | ||||
| -rw-r--r-- | interp/stdarg.ml | 5 | ||||
| -rw-r--r-- | interp/stdarg.mli | 5 |
4 files changed, 32 insertions, 0 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ead4e39692..20ee7aa4fb 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -82,3 +82,13 @@ let () = register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp"; register_name0 wit_bindings "Constrarg.wit_bindings"; register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings"; + () + +(** Aliases *) + +let wit_reference = wit_ref +let wit_global = wit_ref +let wit_clause = wit_clause_dft_concl +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern +let wit_redexpr = wit_red_expr diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 5c26af3c2a..1197b85a25 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -72,3 +72,15 @@ val wit_red_expr : val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) 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 + +(** 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 diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 56b995e537..e497c996f7 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -28,3 +28,8 @@ let () = register_name0 wit_bool "Stdarg.wit_bool" let () = register_name0 wit_int "Stdarg.wit_int" let () = register_name0 wit_string "Stdarg.wit_string" let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident" + +(** Aliases for compatibility *) + +let wit_integer = wit_int +let wit_preident = wit_pre_ident diff --git a/interp/stdarg.mli b/interp/stdarg.mli index d8904dab87..e1f648d7fc 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type val wit_string : string uniform_genarg_type val wit_pre_ident : string uniform_genarg_type + +(** Aliases for compatibility *) + +val wit_integer : int uniform_genarg_type +val wit_preident : string uniform_genarg_type |