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.mli | |
| 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.mli')
| -rw-r--r-- | vernac/egramml.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/egramml.mli b/vernac/egramml.mli index a5ee036db5..c4f4fcfaa4 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -26,6 +26,8 @@ val extend_vernac_command_grammar : val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list +val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type + (** Utility function reused in Egramcoq : *) val make_rule : |