From 648483fe2ff3942b9f2f2cbbf7a0552b8e1997c4 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 21 Feb 2018 16:04:06 -0800
Subject: Rename release_lexer_state to the more descriptive get_lexer_state.

---
 parsing/cLexer.ml4 | 3 ++-
 parsing/cLexer.mli | 2 ++
 parsing/pcoq.ml    | 6 +++---
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index f26398fa92..52a6fe16c6 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -404,8 +404,9 @@ let set_lexer_state (o,s,b,c,f) =
   between_commands := b;
   comments := c;
   current_file := f
-let release_lexer_state () =
+let get_lexer_state () =
   (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
+let release_lexer_state = get_lexer_state
 let drop_lexer_state () =
     set_lexer_state (init_lexer_state Loc.ToplevelInput)
 
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index d3ef19873f..5f4e10f145 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -51,7 +51,9 @@ type lexer_state
 
 val init_lexer_state : Loc.source -> lexer_state
 val set_lexer_state : lexer_state -> unit
+val get_lexer_state : unit -> lexer_state
 val release_lexer_state : unit -> lexer_state
+[@@ocaml.deprecated "Use get_lexer_state"]
 val drop_lexer_state : unit -> unit
 
 (* Retrieve the comments lexed at a given location of the stream
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 54e7949aea..73e1039951 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -111,7 +111,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
     let state = ref (CLexer.init_lexer_state file) in
     CLexer.set_lexer_state !state;
     let a = parsable c in
-    state := CLexer.release_lexer_state ();
+    state := CLexer.get_lexer_state ();
     (a,state)
 
   let action = Gramext.action
@@ -121,7 +121,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
     CLexer.set_lexer_state !state;
     try
       let c = Entry.parse e p in
-      state := CLexer.release_lexer_state ();
+      state := CLexer.get_lexer_state ();
       c
     with Ploc.Exc (loc,e) ->
       CLexer.drop_lexer_state ();
@@ -133,7 +133,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
     CLexer.set_lexer_state !state;
     try
       let a = f x in
-      state := CLexer.release_lexer_state ();
+      state := CLexer.get_lexer_state ();
       a
     with e ->
       CLexer.drop_lexer_state ();
-- 
cgit v1.2.3


From d2293c3e1d51bdd2c25b203c655cc499e9bd5a91 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 22 Feb 2018 09:42:59 -0800
Subject: Tweak developer documentation.

---
 dev/doc/build-system.txt | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 1c4fd2eba4..fd3101613a 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -143,7 +143,9 @@ file list(s):
    These files are also used by the experimental ocamlbuild plugin,
    which is quite touchy about them : be careful with order,
    duplicated entries, whitespace errors, and do not mention .mli there.
- - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+   If module B depends on module A, then B should be after A in the .mllib
+   file.
+- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
  - The definitions in Makefile.common might have to be adapted too.
  - If your file needs a specific rule, add it to Makefile.build
 
-- 
cgit v1.2.3