aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-09 16:33:21 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-09 16:35:49 +0200
commita66b57ba4bba866bb626bde2b6fe3b762347eb3e (patch)
tree7e78979db8010c5221352cb7fcbcc12a8be3db62 /parsing/g_vernac.ml4
parentb43956fe19177a178dfbcef0b173ebada5060973 (diff)
Rename Lexer -> CLexer.
Diffstat (limited to 'parsing/g_vernac.ml4')
-rw-r--r--parsing/g_vernac.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f3766a7d7..b19ad8807 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -27,7 +27,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 *)