diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 18:27:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 21:19:00 +0100 |
| commit | 36e865119e5bb5fbaed14428fc89ecd4e96fb7be (patch) | |
| tree | d0b5d54783126a603bfab7ec2f5950705e414529 /plugins/funind | |
| 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 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 4bd69b9fe..e93c395e3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -94,7 +94,7 @@ let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected." -ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat +ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END |