diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 16:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 21:08:26 +0100 |
| commit | 4b2cdf733df6dc23247b078679e71da98e54f5cc (patch) | |
| tree | ac05560456999b14a897e1701ae6678ab5c6e6b7 /interp | |
| parent | 4d13842869647790c9bd3084dce672fee7b648a1 (diff) | |
Removing the special status of generic entries defined by Coq itself.
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
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 ead4e3969..20ee7aa4f 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 5c26af3c2..1197b85a2 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 56b995e53..e497c996f 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 d8904dab8..e1f648d7f 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 |