diff options
author | 2016-05-09 18:37:29 +0200 | |
---|---|---|
committer | 2016-05-09 18:40:35 +0200 | |
commit | cd9f2859e69d99aea5b29a6d677448a39a234b6f (patch) | |
tree | 500a8b0d1c36662f590c7956cf932663028186be /parsing | |
parent | 4114926d5bf60b014c363788d043c00184655da2 (diff) | |
parent | aa6a7fc837f8148655c179e9a0b63c3044edfe71 (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.ml4 | 2 | ||||
-rw-r--r-- | parsing/egramcoq.ml | 6 | ||||
-rw-r--r-- | parsing/egramml.ml | 2 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
-rw-r--r-- | parsing/parsing.mllib | 2 | ||||
-rw-r--r-- | parsing/pcoq.ml | 4 |
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 |