aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-31 13:33:01 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-31 13:33:01 +0200
commit27dffdea5b46f6282c1584db0555213e744352fa (patch)
tree3f89cd9e8828f1ca1c8a1c10d74f020dcb7543f1 /toplevel/coqtop.ml
parentcb31cd671a0ef4da0cf834dad5b67776098bb0d1 (diff)
Revert "Rename Lexer -> CLexer."
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 08b38a703..9e1a76bbd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -230,11 +230,11 @@ let compile_files () =
| [vf] -> compile_file vf (* One compilation : no need to save init state *)
| l ->
let init_state = States.freeze ~marshallable:`No in
- let coqdoc_init_state = CLexer.location_table () in
+ let coqdoc_init_state = Lexer.location_table () in
List.iter
(fun vf ->
States.unfreeze init_state;
- CLexer.restore_location_table coqdoc_init_state;
+ Lexer.restore_location_table coqdoc_init_state;
compile_file vf)
(List.rev l)