aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/toplevel.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-22 16:03:45 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-22 16:03:45 +0000
commita71ef213674180c17bc707e4eff174c16ebec756 (patch)
tree866ade5f3744c88ef887fb4e564792151f817701 /toplevel/toplevel.ml
parent39836aec4cab3acbb80f0201958d9554b1760f64 (diff)
Fixing camlp4 compilation w.r.t previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15481 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/toplevel.ml')
-rw-r--r--toplevel/toplevel.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index feaa8c970..ad7ad014a 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -322,7 +322,7 @@ let parse_to_dot =
let rec discard_to_dot () =
try
Gram.entry_parse parse_to_dot top_buffer.tokens
- with Loc.Exc_located(_,(Token.Error _|Lexer.Error.E _)) ->
+ with Loc.Exc_located(_,(Compat.Token.Error _|Lexer.Error.E _)) ->
discard_to_dot()