Added an indirection with respect to Loc in Compat. As many [open Compat]

were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.

This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 66 insertions, 70 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 61bc1ae7c9..57987ef41a 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -59,7 +59,7 @@ exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
 
-let dl = dummy_loc
+let dl = Loc.ghost
 
 (* Some pre declaration of constant we are going to use *)
 let bb = constr_of_global Coqlib.glob_bool
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
index f6c69d8902..bfd3c47a06 100644
--- a/toplevel/backtrack.mli
+++ b/toplevel/backtrack.mli
@@ -61,7 +61,7 @@ val reset_initial : unit -> unit
 
 (** Reset to the last known state just before defining [id] *)
 
-val reset_name : Names.identifier Pp.located -> unit
+val reset_name : Names.identifier Loc.located -> unit
 
 (** When a proof is ended (via either Qed/Admitted/Restart/Abort),
     old proof steps should be marked differently to avoid jumping back
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 281ae784e7..849bd7ce26 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
 open Pp
 open Errors
 open Util
@@ -16,10 +15,10 @@ open Pretype_errors
 open Indrec
 
 let print_loc loc =
-  if loc = dummy_loc then
+  if loc = Loc.ghost then
     (str"<unknown>")
   else
-    let loc = unloc loc in
+    let loc = Loc.unloc loc in
     (int (fst loc) ++ str"-" ++ int (snd loc))
 
 let guill s = "\""^s^"\""
@@ -43,7 +42,7 @@ let explain_exn_default = function
   | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
   (* Meta-exceptions *)
   | Loc.Exc_located (loc,exc) ->
-      hov 0 ((if loc = dummy_loc then (mt ())
+      hov 0 ((if loc = Loc.ghost then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
                ++ Errors.print_no_anomaly exc)
   | EvaluatedError (msg,None) -> msg
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 75d742ce18..9a50da7475 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -8,7 +8,7 @@
 
 (** Error report. *)
 
-val print_loc : Pp.loc -> Pp.std_ppcmds
+val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 31a02758f1..fa2f2e168c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -69,7 +69,7 @@ let existing_instance glob g =
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
-type binder_list = (identifier located * bool * constr_expr) list
+type binder_list = (identifier Loc.located * bool * constr_expr) list
 
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
@@ -135,13 +135,13 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	  (fun avoid (clname, (id, _, t)) ->
 	    match clname with
 	    | Some (cl, b) ->
-		let t = CHole (Pp.dummy_loc, None) in
+		let t = CHole (Loc.ghost, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
     | Explicit -> cl, Idset.empty
   in
-  let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
+  let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in
   let k, cty, ctx', ctx, len, imps, subst =
     let impls, ((env', ctx), imps) = interp_context_evars evars env ctx in
     let c', imps' = interp_type_evars_impls ~impls ~evdref:evars ~fail_evar:false env' tclass in
@@ -232,7 +232,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       (CHole (Pp.dummy_loc, Some Evar_kinds.GoalEvar) :: props), rest
+		       (CHole (Loc.ghost, Some Evar_kinds.GoalEvar) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
@@ -348,6 +348,6 @@ let context l =
 	   match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
       in
 	Command.declare_assumption false (Local (* global *), Definitional) t
-	  [] impl (* implicit *) None (* inline *) (dummy_loc, id))
+	  [] impl (* implicit *) None (* inline *) (Loc.ghost, id))
   in List.iter fn (List.rev ctx)
        
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3d97e544ea..e8e6516187 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -355,7 +355,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun ((_,indname),_,ar,lc) -> {
     ind_name = indname;
-    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc,GType None)) ar;
+    ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType None)) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
 
@@ -481,7 +481,7 @@ let check_mutuality env isfix fixl =
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
-  fix_annot : identifier located option;
+  fix_annot : identifier Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
@@ -563,7 +563,7 @@ let mkSubset name typ prop =
 	 [| typ; mkLambda (name, typ, prop) |])
 let sigT = Lazy.lazy_from_fun build_sigma_type
 
-let make_qref s = Qualid (dummy_loc, qualid_of_string s)
+let make_qref s = Qualid (Loc.ghost, qualid_of_string s)
 let lt_ref = make_qref "Init.Peano.lt"
 
 let rec telescope = function
@@ -687,7 +687,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     mkApp (constr_of_global (delayed_force fix_sub_ref),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar isevars env 
-	       ~src:(dummy_loc, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop ; intern_body_lam |])
   in
   let _ = isevars := Evarutil.nf_evar_map !isevars in
@@ -807,7 +807,7 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
-    let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in
+    let indexes = search_guard Loc.ghost (Global.env()) indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let fixdecls =
       list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
@@ -915,7 +915,7 @@ let do_program_recursive fixkind fixl ntns =
 	Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
       in
       let indexes = 
-	Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
 	list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
     end;
     Obligations.add_mutual_definitions defs ntns fixkind
diff --git a/toplevel/command.mli b/toplevel/command.mli
index a43f2ad371..c4b0dba8a2 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -49,9 +49,9 @@ val interp_assumption :
 
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   Impargs.manual_implicits ->
-  bool (** implicit *) -> Entries.inline -> variable located -> unit
+  bool (** implicit *) -> Entries.inline -> variable Loc.located -> unit
 
-val declare_assumptions : variable located list ->
+val declare_assumptions : variable Loc.located list ->
   coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits ->
   bool -> Entries.inline -> unit
 
@@ -99,7 +99,7 @@ val do_mutual_inductive :
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
-  fix_annot : identifier located option;
+  fix_annot : identifier Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e0923cda0a..be8fbf89d1 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1002,12 +1002,12 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	     Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
        | Proof_type.LtacAtomCall (te,otac) -> quote
 	   (Pptactic.pr_glob_tactic (Global.env())
-	      (Tacexpr.TacAtom (dummy_loc,te)))
+	      (Tacexpr.TacAtom (Loc.ghost,te)))
 	   ++ (match !otac with
 		 | Some te' when (Obj.magic te' <> te) ->
 		     strbrk " (expanded to " ++ quote
 		       (Pptactic.pr_tactic (Global.env())
-			  (Tacexpr.TacAtom (dummy_loc,te')))
+			  (Tacexpr.TacAtom (Loc.ghost,te')))
 		     ++ str ")"
 		 | _ -> mt ())
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 7607bda42c..b2f1059262 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -38,7 +38,7 @@ val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
 val explain_ltac_call_trace :
-  int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Pp.loc ->
+  int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Loc.t ->
   std_ppcmds
 
 val explain_module_error : Modops.module_typing_error -> std_ppcmds
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 5ffbedcd7e..b7a6af4948 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -8,7 +8,6 @@
 
 open Vernacexpr
 open Names
-open Compat
 open Errors
 open Util
 open Pp
@@ -366,8 +365,8 @@ let eval_call c =
       | Errors.Quit -> None, "Quit is not allowed by coqide!"
       | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
       | Error_in_file (_,_,inner) -> None, pr_exn inner
-      | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner
-      | Loc.Exc_located (loc, inner) -> Some (Pp.unloc loc), pr_exn inner
+      | Loc.Exc_located (loc, inner) when loc = Loc.ghost -> None, pr_exn inner
+      | Loc.Exc_located (loc, inner) -> Some (Loc.unloc loc), pr_exn inner
       | e -> None, pr_exn e
   in
   let interruptible f x =
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index dc3e0dc474..f9e58a4329 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -334,7 +334,7 @@ requested
               | InType -> recs ^ "t_nodep")
         ) in
         let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
-        let newref = (dummy_loc,newid) in
+        let newref = (Loc.ghost,newid) in
           ((newref,isdep,ind,z)::l1),l2
       in
 	match t with
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 5a4dbabb6d..74b8890ecd 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Loc
 open Pp
 open Names
 open Term
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 31f5d29943..c2891e0c10 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -56,7 +56,7 @@ let adjust_guardness_conditions const = function
 	  lemma_guard (Array.to_list fixdefs) in
 *)
       let indexes =
-	search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
+	search_guard Loc.ghost (Global.env()) possible_indexes fixdecls in
       { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
   | c -> const
 
diff --git a/toplevel/locality.mli b/toplevel/locality.mli
index 5e8d45d87f..6c2194cfe1 100644
--- a/toplevel/locality.mli
+++ b/toplevel/locality.mli
@@ -8,7 +8,7 @@
 
 (** * Managing locality *)
 
-val locality_flag : (Pp.loc * bool) option ref
+val locality_flag : (Loc.t * bool) option ref
 val check_locality : unit -> unit
 
 (** * Extracting the locality flag *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fe1cd7eb32..fee4fef182 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1144,7 +1144,7 @@ let add_notation local c ((loc,df),modifiers) sc =
 
 (* Infix notations *)
 
-let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
+let inject_var x = CRef (Ident (Loc.ghost, id_of_string x))
 
 let add_infix local ((loc,inf),modifiers) pr sc =
   check_infix_modifiers modifiers;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 1b1c61a082..0d6bc39f31 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -13,7 +13,6 @@ open Util
 open Evd
 open Declare
 open Proof_type
-open Compat
 
 (**
    - Get types of existentials ;
@@ -61,7 +60,7 @@ type oblinfo =
     ev_hyps: named_context;
     ev_status: Evar_kinds.obligation_definition_status;
     ev_chop: int option;
-    ev_src: Evar_kinds.t located;
+    ev_src: Evar_kinds.t Loc.located;
     ev_typ: types;
     ev_tac: tactic option;
     ev_deps: Intset.t }
@@ -313,13 +312,13 @@ let explain_no_obligations = function
   | None -> str "No obligations remaining"
 
 type obligation_info =
-    (Names.identifier * Term.types * Evar_kinds.t located *
+    (Names.identifier * Term.types * Evar_kinds.t Loc.located *
      Evar_kinds.obligation_definition_status * Intset.t * tactic option) array
 
 type obligation =
   { obl_name : identifier;
     obl_type : types;
-    obl_location : Evar_kinds.t located;
+    obl_location : Evar_kinds.t Loc.located;
     obl_body : constr option;
     obl_status : Evar_kinds.obligation_definition_status;
     obl_deps : Intset.t;
@@ -329,7 +328,7 @@ type obligation =
 type obligations = (obligation array * int)
 
 type fixpoint_kind =
-  | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of (identifier Loc.located option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
 type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -584,7 +583,7 @@ let declare_mutual_definition l =
       | IsFixpoint wfl ->
 	  let possible_indexes =
 	    list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
-	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+	  let indexes = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
 	    Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
       | IsCoFixpoint ->
 	  None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
@@ -628,7 +627,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
 	assert(obls = [||]);
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
-	       obl_location = dummy_loc, Evar_kinds.InternalHole; obl_type = t;
+	       obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
 	       obl_status = Evar_kinds.Expand; obl_deps = Intset.empty;
 	       obl_tac = None } |],
 	mkVar n
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 26e9879740..a867a9372d 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -40,7 +40,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info *
    evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_map -> int ->
   ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
-  (identifier * types * Evar_kinds.t located * Evar_kinds.obligation_definition_status * Intset.t *
+  (identifier * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Intset.t *
       tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
@@ -52,7 +52,7 @@ val eterm_obligations : env -> identifier -> evar_map -> int ->
        translation from obligation identifiers to constrs, new term, new type *)
 
 type obligation_info =
-  (identifier * Term.types * Evar_kinds.t located *
+  (identifier * Term.types * Evar_kinds.t Loc.located *
       Evar_kinds.obligation_definition_status * Intset.t * tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
@@ -80,7 +80,7 @@ type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type fixpoint_kind =
-  | IsFixpoint of (identifier located option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of (identifier Loc.located option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
 val add_mutual_definitions :
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7991d0e582..feaa8c9700 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -13,7 +13,6 @@ open Flags
 open Cerrors
 open Vernac
 open Pcoq
-open Compat
 
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
@@ -124,7 +123,7 @@ let blanch_utf8_string s bp ep =
   String.sub s' 0 !j
 
 let print_highlight_location ib loc =
-  let (bp,ep) = unloc loc in
+  let (bp,ep) = Loc.unloc loc in
   let bp = bp - ib.start
   and ep = ep - ib.start in
   let highlight_lines =
@@ -146,7 +145,7 @@ let print_highlight_location ib loc =
                       str sn ++ str dn) in
 	  (l1 ++ li ++ ln)
   in
-  let loc = make_loc (bp,ep) in
+  let loc = Loc.make_loc (bp,ep) in
   (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++
      highlight_lines ++ fnl ())
 
@@ -154,7 +153,7 @@ let print_highlight_location ib loc =
 
 let print_location_in_file s inlibrary fname loc =
   let errstrm = str"Error while reading " ++ str s in
-  if loc = dummy_loc then
+  if loc = Loc.ghost then
     hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
   else
     let errstrm =
@@ -163,7 +162,7 @@ let print_location_in_file s inlibrary fname loc =
       hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++
              str"characters " ++ Cerrors.print_loc loc) ++ fnl ()
     else
-      let (bp,ep) = unloc loc in
+      let (bp,ep) = Loc.unloc loc in
       let ic = open_in fname in
       let rec line_of_pos lin bol cnt =
         if cnt < bp then
@@ -178,7 +177,7 @@ let print_location_in_file s inlibrary fname loc =
         hov 0 (* No line break so as to follow emacs error message format *)
           (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
            str", line " ++ int line ++ str", characters " ++
-           Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++
+           Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++
         fnl ()
       with e ->
         (close_in ic;
@@ -192,15 +191,15 @@ let print_command_location ib dloc =
     | None -> (mt ())
 
 let valid_loc dloc loc =
-  loc <> dummy_loc
+  loc <> Loc.ghost
   & match dloc with
     | Some dloc ->
-	let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed
+	let (bd,ed) = Loc.unloc dloc in let (b,e) = Loc.unloc loc in bd<=b & e<=ed
     | _ -> true
 
 let valid_buffer_loc ib dloc loc =
   valid_loc dloc loc &
-  let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
+  let (b,e) = Loc.unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
 
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
     otherwise. We trap all exceptions to prevent the error message printing
@@ -283,7 +282,7 @@ let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
       | DuringCommandInterp (loc,ie) ->
-          if loc = dummy_loc then (None,ie) else (Some loc, ie)
+          if loc = Loc.ghost then (None,ie) else (Some loc, ie)
       | _ -> (None, exc)
   in
   let (locstrm,exc) =
@@ -312,7 +311,7 @@ let print_toplevel_error exc =
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =
-  let rec dot st = match get_tok (Stream.next st) with
+  let rec dot st = match Compat.get_tok (Stream.next st) with
     | Tok.KEYWORD "." -> ()
     | Tok.EOI -> raise End_of_input
     | _ -> dot st
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ac3dd39cbf..a1015d15eb 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -17,13 +17,12 @@ open System
 open Vernacexpr
 open Vernacinterp
 open Ppvernac
-open Compat
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-exception DuringCommandInterp of Pp.loc * exn
+exception DuringCommandInterp of Loc.t * exn
 
 exception HasNotFailed
 
@@ -51,13 +50,13 @@ let raise_with_file file exc =
   let (cmdloc,re) =
     match exc with
       | DuringCommandInterp(loc,e) -> (loc,e)
-      | e -> (dummy_loc,e)
+      | e -> (Loc.ghost,e)
   in
   let (inner,inex) =
     match re with
-      | Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
+      | Error_in_file (_, (b,f,loc), e) when loc <> Loc.ghost ->
           ((b, f, loc), e)
-      | Loc.Exc_located (loc, e) when loc <> dummy_loc ->
+      | Loc.Exc_located (loc, e) when loc <> Loc.ghost ->
           ((false,file, loc), e)
       | Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
   in
@@ -152,7 +151,7 @@ let close_input in_chan (_,verb) =
   with _ -> ()
 
 let verbose_phrase verbch loc =
-  let loc = unloc loc in
+  let loc = Loc.unloc loc in
   match verbch with
     | Some ch ->
 	let len = snd loc - fst loc in
@@ -184,7 +183,7 @@ let set_formatter_translator() =
   Format.set_max_boxes max_int
 
 let pr_new_syntax loc ocom =
-  let loc = unloc loc in
+  let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
   let fs = States.freeze () in
   let com = match ocom with
@@ -308,10 +307,10 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
       | End_of_input ->
-          if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
+          if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname e
 
-(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit]
+(** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
    It executes one vernacular command. By default the command is
    considered as non-state-preserving, in which case we add it to the
    Backtrack stack (triggering a save of a frozen state and the generation
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 79ea1a4c53..924f2a65e9 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,12 +12,12 @@
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
 val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
- Pp.loc * Vernacexpr.vernac_expr
+ Loc.t * Vernacexpr.vernac_expr
 
 (** Reads and executes vernac commands from a stream.
    The boolean [just_parsing] disables interpretation of commands. *)
 
-exception DuringCommandInterp of Pp.loc * exn
+exception DuringCommandInterp of Loc.t * exn
 exception End_of_input
 
 val just_parsing : bool ref
@@ -28,7 +28,7 @@ val just_parsing : bool ref
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-val eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit
+val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
 (** Set XML hooks *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 16cf388b97..da30513c48 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -475,7 +475,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
   in
     Dumpglob.dump_moddef loc mp "mod";
     if_verbose msg_info (str ("Module "^ string_of_id id ^" is declared"));
-    Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+    Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
@@ -499,7 +499,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
          List.iter
            (fun (export,id) ->
              Option.iter
-               (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+               (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
            ) argsexport
     | _::_ ->
        let binders_ast = List.map
@@ -517,7 +517,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose msg_info
 	   (str ("Module "^ string_of_id id ^" is defined"));
-         Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
+         Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
            export
 
 let vernac_end_module export (loc,id as lid) =
@@ -547,7 +547,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
         List.iter
          (fun (export,id) ->
            Option.iter
-            (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+            (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
          ) argsexport
 
     | _ :: _ ->
@@ -1172,7 +1172,7 @@ let vernac_check_may_eval redexp glopt rc =
       Evarutil.check_evars env sigma sigma' c;
       Arguments_renaming.rename_typing env c
     with P.PretypeError (_,_,P.UnsolvableImplicit _)
-      | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) ->
+      | Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) ->
       Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
   match redexp with
     | None ->
@@ -1265,7 +1265,7 @@ let interp_search_about_item = function
   | SearchString (s,sc) ->
       try
 	let ref =
-	  Notation.interp_notation_as_global_reference dummy_loc
+	  Notation.interp_notation_as_global_reference Loc.ghost
 	    (fun _ -> true) s sc in
 	GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->