diff options
| author | Pierre-Marie Pédrot | 2016-03-17 18:27:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 21:19:00 +0100 |
| commit | 36e865119e5bb5fbaed14428fc89ecd4e96fb7be (patch) | |
| tree | d0b5d54783126a603bfab7ec2f5950705e414529 /tactics/extraargs.mli | |
| parent | 4b2cdf733df6dc23247b078679e71da98e54f5cc (diff) | |
Removing the special status of generic arguments defined by Coq itself.
This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They
now have to be reachable in the ML code. Note that this has some consequences,
as the previous macro was potentially mixing grammar entries and arguments as
long as their name was the same. Now, each genarg comes with its grammar
instead, so there is no way to abuse the macro.
Diffstat (limited to 'tactics/extraargs.mli')
| -rw-r--r-- | tactics/extraargs.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index f7b379e69e..14aa69875f 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -21,6 +21,8 @@ val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg val pr_occurrences : int list or_var -> Pp.std_ppcmds val occurrences_of : int list -> Locus.occurrences +val wit_natural : int Genarg.uniform_genarg_type + val wit_glob : (constr_expr, Tacexpr.glob_constr_and_expr, @@ -31,6 +33,11 @@ val wit_lglob : Tacexpr.glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type +val wit_lconstr : + (constr_expr, + Tacexpr.glob_constr_and_expr, + Constr.t) Genarg.genarg_type + val glob : constr_expr Pcoq.Gram.entry val lglob : constr_expr Pcoq.Gram.entry |