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/numeral.mli | |
| 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/numeral.mli')
| -rw-r--r-- | plugins/syntax/numeral.mli | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli index 83ede6f48f..f96b8321f8 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -9,14 +9,9 @@ (************************************************************************) open Libnames -open Constrexpr open Vernacexpr +open Notation (** * Numeral notation *) -type numnot_option = - | Nop - | Warning of raw_natural_number - | Abstract of raw_natural_number - val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit |