diff options
| author | Pierre-Marie Pédrot | 2016-03-17 16:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 21:08:26 +0100 |
| commit | 4b2cdf733df6dc23247b078679e71da98e54f5cc (patch) | |
| tree | ac05560456999b14a897e1701ae6678ab5c6e6b7 /interp/constrarg.mli | |
| 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/constrarg.mli')
| -rw-r--r-- | interp/constrarg.mli | 12 |
1 files changed, 12 insertions, 0 deletions
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 |