From 40d92a65c80a1af0495e8ceed19d74b986ed48c9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Fri, 7 Apr 2017 19:12:18 +0200
Subject: [PATCH] Add a comment about the type [production].
---
src/IncrementalEngine.ml | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/IncrementalEngine.ml b/src/IncrementalEngine.ml
index d6aa9385d..88e556973 100644
--- a/src/IncrementalEngine.ml
+++ b/src/IncrementalEngine.ml
@@ -24,6 +24,12 @@ module type INCREMENTAL_ENGINE = sig
type token
+ (* A value of type [production] is (an index for) a production. The start
+ productions (which do not exist in an \mly file, but are constructed by
+ Menhir internally) are not part of this type. *)
+
+ type production
+
(* The type ['a checkpoint] represents an intermediate or final state of the
parser. An intermediate checkpoint is a suspension: it records the parser's
current state, and allows parsing to be resumed. The parameter ['a] is
@@ -63,8 +69,6 @@ module type INCREMENTAL_ENGINE = sig
type 'a env
- type production
-
type 'a checkpoint = private
| InputNeeded of 'a env
| Shifting of 'a env * 'a env * bool
--
GitLab