aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-09 18:37:29 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-09 18:40:35 +0200
commitcd9f2859e69d99aea5b29a6d677448a39a234b6f (patch)
tree500a8b0d1c36662f590c7956cf932663028186be /parsing
parent4114926d5bf60b014c363788d043c00184655da2 (diff)
parentaa6a7fc837f8148655c179e9a0b63c3044edfe71 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml4 (renamed from parsing/lexer.ml4)0
-rw-r--r--parsing/cLexer.mli (renamed from parsing/lexer.mli)0
-rw-r--r--parsing/compat.ml42
-rw-r--r--parsing/egramcoq.ml6
-rw-r--r--parsing/egramml.ml2
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_prim.ml42
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/parsing.mllib2
-rw-r--r--parsing/pcoq.ml4
11 files changed, 12 insertions, 12 deletions
diff --git a/parsing/lexer.ml4 b/parsing/cLexer.ml4
index 8b8b38c34..8b8b38c34 100644
--- a/parsing/lexer.ml4
+++ b/parsing/cLexer.ml4
diff --git a/parsing/lexer.mli b/parsing/cLexer.mli
index 24b0ec847..24b0ec847 100644
--- a/parsing/lexer.mli
+++ b/parsing/cLexer.mli
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 1747aa535..310a44149 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -135,7 +135,7 @@ let to_coq_position = function
END
-(** Signature of Lexer *)
+(** Signature of CLexer *)
IFDEF CAMLP5 THEN
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 04b622864..eff666c9c 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -265,9 +265,9 @@ let recover_constr_grammar ntn prec =
(* Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
-type frozen_t = (int * GrammarCommand.t) list * Lexer.frozen_t
+type frozen_t = (int * GrammarCommand.t) list * CLexer.frozen_t
-let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
+let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ())
(* We compare the current state of the grammar and the state to unfreeze,
by computing the longest common suffixes *)
@@ -283,7 +283,7 @@ let unfreeze (grams, lex) =
remove_grammars n;
remove_levels n;
grammar_state := common;
- Lexer.unfreeze lex;
+ CLexer.unfreeze lex;
List.iter extend_dyn_grammar (List.rev_map snd redo)
(** No need to provide an init function : the grammar state is
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 95ac87247..97a3e89a5 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -33,7 +33,7 @@ let rec ty_rule_of_gram = function
| [] -> AnyTyRule TyStop
| GramTerminal s :: rem ->
let AnyTyRule rem = ty_rule_of_gram rem in
- let tok = Atoken (Lexer.terminal s) in
+ let tok = Atoken (CLexer.terminal s) in
let r = TyNext (rem, tok, None) in
AnyTyRule r
| GramNonTerminal (_, t, tok) :: rem ->
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7e470e844..243f71416 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -29,7 +29,7 @@ let constr_kw =
"Prop"; "Set"; "Type"; ".("; "_"; "..";
"`{"; "`("; "{|"; "|}" ]
-let _ = List.iter Lexer.add_keyword constr_kw
+let _ = List.iter CLexer.add_keyword constr_kw
let mk_cast = function
(c,(_,None)) -> c
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 5e67e9957..0d72f7b93 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -15,7 +15,7 @@ open Pcoq
open Pcoq.Prim
let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
-let _ = List.iter Lexer.add_keyword prim_kw
+let _ = List.iter CLexer.add_keyword prim_kw
let local_make_qualid l id = make_qualid (DirPath.make l) id
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 0c90a8bca..1a27d9692 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -25,7 +25,7 @@ open Pcoq
let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta]
let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter Lexer.add_keyword tactic_kw
+let _ = List.iter CLexer.add_keyword tactic_kw
let err () = raise Stream.Failure
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 35ba9757d..df42d9084 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -26,7 +26,7 @@ open Pcoq.Vernac_
open Pcoq.Module
let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
-let _ = List.iter Lexer.add_keyword vernac_kw
+let _ = List.iter CLexer.add_keyword vernac_kw
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 024d8607f..b052b6ee6 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,6 @@
Tok
Compat
-Lexer
+CLexer
Entry
Pcoq
Egramml
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fe9ab630f..6dcf76da8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -15,14 +15,14 @@ open Genarg
(** The parser of Coq *)
-module G = GrammarMake (Lexer)
+module G = GrammarMake (CLexer)
let warning_verbose = Compat.warning_verbose
module Symbols = GramextMake(G)
let gram_token_of_token = Symbols.stoken
-let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
+let gram_token_of_string s = gram_token_of_token (CLexer.terminal s)
let camlp4_verbosity silent f x =
let a = !warning_verbose in