From e39c84ff2dc20ce059ee6198e142ca076de8c6cb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Sep 2018 09:22:12 -0400
Subject: 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.
---
 plugins/syntax/numeral.mli | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'plugins/syntax/numeral.mli')

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
-- 
cgit v1.2.3