diff options
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 |