aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-09 13:58:59 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:04 +0100
commit51976c9f2157953f794ed1efcd68403a8545d346 (patch)
tree612cc59179d2d16d5bb552f31f0abda92e50dd23 /interp/notation.mli
parent6901f720c6115c8eec1343846641a5c8453c3268 (diff)
A bit of miscellaneous code documentation around notations.
Diffstat (limited to 'interp/notation.mli')
-rw-r--r--interp/notation.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/notation.mli b/interp/notation.mli
index 7d055571c..d10012212 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