diff options
| author | Jason Gross | 2018-09-19 09:22:12 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-09-19 18:43:02 -0400 |
| commit | e39c84ff2dc20ce059ee6198e142ca076de8c6cb (patch) | |
| tree | dc2836aeb64fdca1895d45f8019031f8c3a1edcf /plugins/syntax/g_numeral.ml4 | |
| parent | df1f5bcd406a87c77601942f21d16555a8f6086e (diff) | |
Fix Numeral Notations (1/4 - moving things)
Move various things from from numeral.ml to notation.ml and
notation.mli; this is required to allow the vernac command to continue
living in numeral.ml while preparing to move all of the numeral notation
interpretation logic to notation.ml
This is commit 1/4 in the fix for #8401.
This is a pure cut/paste commit, modulo adding section-heading comments.
Diffstat (limited to 'plugins/syntax/g_numeral.ml4')
| -rw-r--r-- | plugins/syntax/g_numeral.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index ec14df3baa..55f61a58f9 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -10,6 +10,7 @@ DECLARE PLUGIN "numeral_notation_plugin" +open Notation open Numeral open Pp open Names |