From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 plugins/syntax/number.mli | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 plugins/syntax/number.mli

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

diff --git a/plugins/syntax/number.mli b/plugins/syntax/number.mli
new file mode 100644
index 0000000000..5a13d1068b
--- /dev/null
+++ b/plugins/syntax/number.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Libnames
+open Vernacexpr
+open Notation
+
+(** * Number notation *)
+
+type number_string_via = qualid * (bool * qualid * qualid) list
+type number_option =
+  | After of numnot_option
+  | Via of number_string_via
+
+val vernac_number_notation : locality_flag ->
+                             qualid ->
+                             qualid -> qualid ->
+                             number_option list ->
+                             Notation_term.scope_name -> unit
-- 
cgit v1.2.3


From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:27:00 +0200
Subject: [string notation] Handle parameterized inductives and non inductives

---
 plugins/syntax/number.mli | 5 +++++
 1 file changed, 5 insertions(+)

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

diff --git a/plugins/syntax/number.mli b/plugins/syntax/number.mli
index 5a13d1068b..d7d28b29ed 100644
--- a/plugins/syntax/number.mli
+++ b/plugins/syntax/number.mli
@@ -24,3 +24,8 @@ val vernac_number_notation : locality_flag ->
                              qualid -> qualid ->
                              number_option list ->
                              Notation_term.scope_name -> unit
+
+(** These are also used in string notations *)
+val locate_global_inductive : bool -> Libnames.qualid -> Names.inductive * Names.GlobRef.t option list
+val elaborate_to_post_params : Environ.env -> Evd.evar_map -> Names.inductive -> Names.GlobRef.t option list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list
+val elaborate_to_post_via : Environ.env -> Evd.evar_map -> Libnames.qualid -> Names.inductive -> (bool * Libnames.qualid * Libnames.qualid) list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list
-- 
cgit v1.2.3