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/string_syntax.ml | |
| 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/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions