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

1 files changed, 3 insertions, 1 deletions

diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 52b3149bb..637b427a0 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