From 51976c9f2157953f794ed1efcd68403a8545d346 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Aug 2017 13:58:59 +0200
Subject: A bit of miscellaneous code documentation around notations.

---
 interp/notation.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 7d055571c8..d100122129 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -176,10 +176,10 @@ val scope_class_of_class : Classops.cl_typ -> scope_class
 (** Building notation key *)
 
 type symbol =
-  | Terminal of string
-  | NonTerminal of Id.t
-  | SProdList of Id.t * symbol list
-  | Break of int
+  | Terminal of string              (* an expression including symbols or a simply-quoted ident, e.g. "'U'" or "!" *)
+  | NonTerminal of Id.t             (* an identifier "x" *)
+  | SProdList of Id.t * symbol list (* an expression "x sep .. sep y", remembering x (or y) and sep *)
+  | Break of int                    (* a sequence of blanks > 1, e.g. "   " *)
 
 val symbol_eq : symbol -> symbol -> bool
 
-- 
cgit v1.2.3


From b176959335a8cc097c254ea10b910e8ecbcde54b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 24 Aug 2017 21:14:43 +0200
Subject: More flexibility in locating or referring to a notation.

We generalize the possibility to refer to a notation not only by its
"_ U _" form but also using its "a 'U' b".

(Wish from EJGA)
---
 interp/notation.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index d100122129..a4c79d6d35 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -183,9 +183,13 @@ type symbol =
 
 val symbol_eq : symbol -> symbol -> bool
 
+(** Make/decompose a notation of the form "_ U _" *)
 val make_notation_key : symbol list -> notation
 val decompose_notation_key : notation -> symbol list
 
+(** Decompose a notation of the form "a 'U' b" *)
+val decompose_raw_notation : string -> symbol list
+
 (** Prints scopes (expects a pure aconstr printer) *)
 val pr_scope_class : scope_class -> Pp.t
 val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t
-- 
cgit v1.2.3