diff options
| author | Pierre-Marie Pédrot | 2018-07-11 22:57:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-12 13:53:22 +0200 |
| commit | b9ff36b39eb193757ce57a89afe138cd09e759d7 (patch) | |
| tree | 5c692d9cad8ce9db00c9d7c127750650cd7b26a8 /vernac/egramml.ml | |
| parent | 270ceed48217797e99ec845cc5d1c599b5729bc2 (diff) | |
Statically typecheck the VERNAC EXTEND wrapper.
This moves the typing code from the macro expansion to the extension
registering mechanism, bringing in more static safety. We also seize
the opportunity to remove dead code in the macro.
Diffstat (limited to 'vernac/egramml.ml')
| -rw-r--r-- | vernac/egramml.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 048d4d93a0..c5dedc880e 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -64,6 +64,15 @@ let make_rule f prod = let act = ty_eval ty_rule f in Extend.Rule (symb, act) +let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function +| TUentry a -> ExtraArg a +| TUentryl (a,l) -> ExtraArg a +| TUopt(o) -> OptArg (proj_symbol o) +| TUlist1 l -> ListArg (proj_symbol l) +| TUlist1sep (l,_) -> ListArg (proj_symbol l) +| TUlist0 l -> ListArg (proj_symbol l) +| TUlist0sep (l,_) -> ListArg (proj_symbol l) + (** Vernac grammar extensions *) let vernac_exts = ref [] |