From 3ac6551b239281f2bd985488ad3eb36b9b107115 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 22 Dec 2012 05:10:11 +0000
Subject: Avoiding collision between Camlp4 Loc.Exc_located and Coq's
 Loc.Exc_located.

Also fixing coqmktop for use with Camlp4. Don't know if this is the
fix intended by coqmktop experts or not, though.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16113 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/compat.ml4  | 4 +++-
 scripts/coqmktop.ml | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 52b3149bb8..637b427a03 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -220,6 +220,8 @@ module type GrammarSig = sig
 end
 
 module GrammarMake (L:LexerSig) : GrammarSig = struct
+  (* We need to refer to Coq's module Loc before it is hidden by include *)
+  let raise_coq_loc loc e = raise (Loc.Exc_located (to_coqloc loc,e))
   include Camlp4.Struct.Grammar.Static.Make (L)
   type 'a entry = 'a Entry.t
   type action = Action.t
@@ -229,7 +231,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   let entry_create = Entry.mk
   let entry_parse e s =
     try parse e (*FIXME*)CompatLoc.ghost s
-    with Exc_located (loc,e) -> raise (Loc.Exc_located (to_coqloc loc,e))
+    with Exc_located (loc,e) -> raise_coq_loc loc e
   let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 76548aa3d6..9220605e85 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -46,7 +46,7 @@ let camlp4topobjs =
       "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
       "Camlp4Parsers/Camlp4OCamlParser.cmo";
       "Camlp4Parsers/Camlp4GrammarParser.cmo";
-      "q_util.cmo"; "q_coqast.cmo" ]
+      "grammar/q_util.cmo"; "grammar/q_coqast.cmo" ]
 let topobjs = camlp4topobjs
 
 let gramobjs = []
-- 
cgit v1.2.3