Merge branch 'v8.6'

21 files changed, 392 insertions, 241 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2792e5756a..faf4b4c31b 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -52,6 +52,11 @@ important things:
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
+** Parsing **
+
+Pcoq.parsable now takes an extra optional filename argument so as to
+bind locations to a file name when relevant.
+
 ** Files **
 
 To avoid clashes with OCaml's compiler libs, the following files were renamed:
diff --git a/lib/flags.ml b/lib/flags.ml
index 08001f0e7a..b2407a3b78 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -143,8 +143,6 @@ let pr_version = function
 
 (* Translate *)
 let beautify = ref false
-let make_beautify f = beautify := f
-let do_beautify () = !beautify
 let beautify_file = ref false
 
 (* Silent / Verbose *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 67c99a38d8..bd365e6538 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -70,8 +70,6 @@ val version_less_or_equal : compat_version -> bool
 val pr_version : compat_version -> string
 
 val beautify : bool ref
-val make_beautify : bool -> unit
-val do_beautify : unit -> bool
 val beautify_file : bool ref
 
 val make_silent : bool -> unit
diff --git a/lib/unicode.ml b/lib/unicode.ml
index dc852d9819..ced5e258c2 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -8,9 +8,7 @@
 
 (** Unicode utilities *)
 
-type status = Letter | IdentPart | Symbol
-
-exception Unsupported
+type status = Letter | IdentPart | Symbol | Unknown
 
 (* The following table stores classes of Unicode characters that
    are used by the lexer. There are 3 different classes so 2 bits are
@@ -29,6 +27,7 @@ let mask i = function
   | Letter    -> 1 lsl ((i land 7) lsl 1) (* 01 *)
   | IdentPart -> 2 lsl ((i land 7) lsl 1) (* 10 *)
   | Symbol    -> 3 lsl ((i land 7) lsl 1) (* 11 *)
+  | Unknown   -> 0 lsl ((i land 7) lsl 1) (* 00 *)
 
 (* Helper to reset 2 bits in a word. *)
 let reset_mask i =
@@ -55,7 +54,7 @@ let lookup x =
     if      v = 1 then Letter
     else if v = 2 then IdentPart
     else if v = 3 then Symbol
-    else raise Unsupported
+    else Unknown
 
 (* [classify] discriminates between 3 different kinds of
    symbols based on the standard unicode classification (extracted from
@@ -215,7 +214,6 @@ let ident_refutation s =
         |x -> x
   with
   | End_of_input -> Some (true,"The empty string is not an identifier.")
-  | Unsupported -> Some (true,s^": unsupported character in utf8 sequence.")
   | Invalid_argument _ -> Some (true,s^": invalid utf8 sequence.")
 
 let lowercase_unicode =
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 1f8bd44eee..2609e1968f 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -8,22 +8,16 @@
 
 (** Unicode utilities *)
 
-type status = Letter | IdentPart | Symbol
+type status = Letter | IdentPart | Symbol | Unknown
 
-(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *)
-exception Unsupported
-
-(** Classify a unicode char into 3 classes.
-    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
+(** Classify a unicode char into 3 classes or unknown. *)
 val classify : int -> status
 
 (** Return [None] if a given string can be used as a (Coq) identifier.
-    Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity.
-    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
+    Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *)
 val ident_refutation : string -> (bool * string) option
 
 (** First char of a string, converted to lowercase
-    @raise Unsupported if the input string contains unsupported UTF-8 characters.
     @raise Assert_failure if the input string is empty. *)
 val lowercase_first_char : string -> string
 
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index a7b413f57c..98d54240ba 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -101,14 +101,6 @@ module Error = struct
 end
 open Error
 
-let current_file = ref ""
-
-let get_current_file () =
-  !current_file
-
-let set_current_file ~fname =
-  current_file := fname
-
 let err loc str = Loc.raise ~loc:(Compat.to_coqloc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
@@ -120,11 +112,6 @@ type token_kind =
   | AsciiChar
   | EmptyStream
 
-let error_unsupported_unicode_character loc n unicode cs =
-  let bp = Stream.count cs in
-  let loc = set_loc_pos loc bp (bp+n) in
-  err loc (UnsupportedUnicode unicode)
-
 let error_utf8 loc cs =
   let bp = Stream.count cs in
   Stream.junk cs; (* consume the char to avoid read it and fail again *)
@@ -174,14 +161,12 @@ let lookup_utf8_tail loc c cs =
           (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F)
       | _ -> error_utf8 loc cs
     in
-    try Unicode.classify unicode, n
-    with Unicode.Unsupported ->
-      njunk n cs; error_unsupported_unicode_character loc n unicode cs
+    Utf8Token (Unicode.classify unicode, n)
 
 let lookup_utf8 loc cs =
   match Stream.peek cs with
     | Some ('\x00'..'\x7F') -> AsciiChar
-    | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail loc c cs)
+    | Some ('\x80'..'\xFF' as c) -> lookup_utf8_tail loc c cs
     | None -> EmptyStream
 
 let unlocated f x = f x
@@ -199,17 +184,6 @@ let check_keyword str =
   in
   loop_symb (Stream.of_string str)
 
-let warn_unparsable_keyword =
-  CWarnings.create ~name:"unparsable-keyword" ~category:"parsing"
-         (fun (s,unicode) ->
-          strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
-                                  which will not be parsable." s unicode))
-            
-let check_keyword_to_add s =
-  try check_keyword s
-  with Error.E (UnsupportedUnicode unicode) ->
-    warn_unparsable_keyword (s,unicode)
-
 let check_ident str =
   let rec loop_id intail = parser
     | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] ->
@@ -240,7 +214,7 @@ let is_keyword s =
 let add_keyword str =
   if not (is_keyword str) then
     begin
-      check_keyword_to_add str;
+      check_keyword str;
       token_tree := ttree_add !token_tree str
     end
 
@@ -270,6 +244,12 @@ let get_buff len = String.sub !buff 0 len
 
 (* The classical lexer: idents, numbers, quoted strings, comments *)
 
+let warn_unrecognized_unicode =
+  CWarnings.create ~name:"unrecognized-unicode" ~category:"parsing"
+         (fun (u,id) ->
+          strbrk (Printf.sprintf "Not considering unicode character \"%s\" of unknown \
+                                  lexical status as part of identifier \"%s\"." u id))
+
 let rec ident_tail loc len = parser
   | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] ->
       ident_tail loc (store len c) s
@@ -277,6 +257,10 @@ let rec ident_tail loc len = parser
       match lookup_utf8 loc s with
       | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) ->
           ident_tail loc (nstore n len s) s
+      | Utf8Token (Unicode.Unknown, n) ->
+          let id = get_buff len in
+          let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in
+          warn_unrecognized_unicode ~loc:!@loc (u,id); len
       | _ -> len
 
 let rec number len = parser
@@ -334,6 +318,9 @@ let rec string loc ~comm_level bp len = parser
 (* Hook for exporting comment into xml theory files *)
 let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
 
+(* To associate locations to a file name *)
+let current_file = ref None
+
 (* Utilities for comments in beautify *)
 let comment_begin = ref None
 let comm_loc bp = match !comment_begin with
@@ -354,16 +341,20 @@ let rec split_comments comacc acc pos = function
 
 let extract_comments pos = split_comments [] [] pos !comments
 
-type comments_state = int option * string * bool * ((int * int) * string) list
-let restore_comments_state (o,s,b,c) =
+(* The state of the lexer visible from outside *)
+type lexer_state = int option * string * bool * ((int * int) * string) list * string option
+
+let init_lexer_state f = (None,"",true,[],f)
+let set_lexer_state (o,s,b,c,f) =
   comment_begin := o;
   Buffer.clear current_comment; Buffer.add_string current_comment s;
   between_commands := b;
-  comments := c
-let default_comments_state = (None,"",true,[])
-let comments_state () =
-  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in
-  restore_comments_state default_comments_state; s
+  comments := c;
+  current_file := f
+let release_lexer_state () =
+  (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
+let drop_lexer_state () =
+    set_lexer_state (init_lexer_state None)
 
 let real_push_char c = Buffer.add_char current_comment c
 
@@ -391,7 +382,7 @@ let comment_stop ep =
   if !Flags.xml_export && Buffer.length current_comment > 0 &&
     (!between_commands || not(null_comment current_s)) then
       Hook.get f_xml_output_comment current_s;
-  (if Flags.do_beautify() && Buffer.length current_comment > 0 &&
+  (if !Flags.beautify && Buffer.length current_comment > 0 &&
     (!between_commands || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
@@ -408,7 +399,7 @@ let comment_stop ep =
 
 (* Does not unescape!!! *)
 let rec comm_string loc bp = parser
-  | [< ''"' >] ep -> push_string "\""; loc
+  | [< ''"' >] -> push_string "\""; loc
   | [< ''\\'; loc =
            (parser [< ' ('"' | '\\' as c) >] ->
               let () = match c with
@@ -438,7 +429,7 @@ let rec comment loc bp = parser bp2
       let loc =
 	(* In beautify mode, the lexing differs between strings in comments and
 	   regular strings (e.g. escaping). It seems wrong. *)
-	if Flags.do_beautify() then (push_string"\""; comm_string loc bp2 s)
+	if !Flags.beautify then (push_string"\""; comm_string loc bp2 s)
 	else fst (string loc ~comm_level:(Some 0) bp2 0 s)
       in
       comment loc bp s
@@ -511,20 +502,19 @@ let process_chars loc bp c cs =
 	let loc = set_loc_pos loc bp ep' in
         err loc Undefined_token
 
-let token_of_special c s = match c with
-  | '.' -> FIELD s
-  | _ -> assert false
+(* Parse what follows a dot *)
 
-(* Parse what follows a dot / a dollar *)
-
-let parse_after_special loc c bp =
+let parse_after_dot loc c bp =
   parser
-  | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d) >] ->
-      token_of_special c (get_buff len)
+  | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d); s >] ->
+      let field = get_buff len in
+      (try find_keyword loc ("."^field) s with Not_found -> FIELD field)
   | [< s >] ->
       match lookup_utf8 loc s with
       | Utf8Token (Unicode.Letter, n) ->
-          token_of_special c (get_buff (ident_tail loc (nstore n 0 s) s))
+          let len = ident_tail loc (nstore n 0 s) s in
+          let field = get_buff len in
+          (try find_keyword loc ("."^field) s with Not_found -> FIELD field)
       | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s)
 
 (* Parse what follows a question mark *)
@@ -552,7 +542,7 @@ let rec next_token loc = parser bp
       comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s
   | [< '' ' | '\t' | '\r' as c; s >] ->
       comm_loc bp; push_char c; next_token loc s
-  | [< ''.' as c; t = parse_after_special loc c bp; s >] ep ->
+  | [< ''.' as c; t = parse_after_dot loc c bp; s >] ep ->
       comment_stop bp;
       (* We enforce that "." should either be part of a larger keyword,
          for instance ".(", or followed by a blank or eof. *)
@@ -600,7 +590,7 @@ let rec next_token loc = parser bp
             let ep = Stream.count s in
             comment_stop bp;
             (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
-        | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) ->
+        | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) ->
             let t = process_chars loc bp (Stream.next s) s in
             let new_between_commands = match t with
               (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in
@@ -626,12 +616,6 @@ let loct_func loct i =
 
 let loct_add loct i loc = Hashtbl.add loct i loc
 
-let current_location_table = ref (loct_create ())
-
-type location_table = (int, Compat.CompatLoc.t) Hashtbl.t
-let location_table () = !current_location_table
-let restore_location_table t = current_location_table := t
-
 (** {6 The lexer of Coq} *)
 
 (** Note: removing a token.
@@ -669,7 +653,6 @@ let func cs =
 	 cur_loc := Compat.after loc;
          loct_add loct i loc; Some tok)
   in
-  current_location_table := loct;
   (ts, loct_func loct)
 
 let lexer = {
@@ -706,7 +689,6 @@ end
 let mk () =
   let loct = loct_create () in
   let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
-  current_location_table := loct; 
   let rec self init_loc (* FIXME *) =
     parser i
        [< (tok, loc) = next_token !cur_loc; s >] ->
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3ad49eb74a..f69d953354 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -10,22 +10,6 @@ val add_keyword : string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
 
-(* val location_function : int -> Loc.t *)
-
-(** for coqdoc *)
-type location_table
-val location_table : unit -> location_table
-val restore_location_table : location_table -> unit
-
-
-(** [get_current_file fname] returns the filename used in locations emitted by
-    the lexer *)
-val get_current_file : unit -> string
-
-(** [set_current_file fname] sets the filename used in locations emitted by the
-    lexer *)
-val set_current_file : fname:string -> unit
-
 val check_ident : string -> unit
 val is_ident : string -> bool
 val check_keyword : string -> unit
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 58b74da26a..4a36af2d80 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -10,6 +10,10 @@
 
 (** Locations *)
 
+let file_loc_of_file = function
+| None -> ""
+| Some f -> f
+
 IFDEF CAMLP5 THEN
 
 module CompatLoc = struct
@@ -29,7 +33,7 @@ let to_coqloc loc =
     Loc.line_nb_last = Ploc.line_nb_last loc;
     Loc.bol_pos_last = Ploc.bol_pos_last loc; }
 
-let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc fname line_nb bol_pos (bp, ep) ""
+let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""
 
 (* Update a loc without allocating an intermediate pair *)
 let set_loc_pos loc bp ep =
@@ -80,7 +84,7 @@ let to_coqloc loc =
     Loc.bol_pos_last = CompatLoc.stop_bol loc; }
 
 let make_loc fname line_nb bol_pos start stop =
-  CompatLoc.of_tuple (fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
+  CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
 
 open CompatLoc
 
@@ -97,7 +101,7 @@ let bump_loc_line_last loc bol_pos =
 	    stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc)
 
 let set_loc_file loc fname =
-  of_tuple (fname, start_line loc, start_bol loc, start_off loc,
+  of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc,
 	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)
 
 let after loc =
@@ -138,20 +142,22 @@ module type LexerSig = sig
     exception E of t
     val to_string : t -> string
   end
-  type comments_state
-  val default_comments_state : comments_state
-  val comments_state : unit -> comments_state
-  val restore_comments_state : comments_state -> unit
+  type lexer_state
+  val init_lexer_state : string option -> lexer_state
+  val set_lexer_state : lexer_state -> unit
+  val release_lexer_state : unit -> lexer_state
+  val drop_lexer_state : unit -> unit
 end
 
 ELSE
 
 module type LexerSig = sig
   include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
-  type comments_state
-  val default_comments_state : comments_state
-  val comments_state : unit -> comments_state
-  val restore_comments_state : comments_state -> unit
+  type lexer_state
+  val init_lexer_state : string option -> lexer_state
+  val set_lexer_state : lexer_state -> unit
+  val release_lexer_state : unit -> lexer_state
+  val drop_lexer_state : unit -> unit
 end
 
 END
@@ -172,7 +178,7 @@ module type GrammarSig = sig
   type extend_statment =
       Gramext.position option * single_extend_statment list
   type coq_parsable
-  val parsable : char Stream.t -> coq_parsable
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -193,32 +199,34 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
-  type coq_parsable = parsable * L.comments_state ref
-  let parsable c =
-    let state = ref L.default_comments_state in (parsable c, state)
+  type coq_parsable = parsable * L.lexer_state ref
+  let parsable ?file c =
+    let state = ref (L.init_lexer_state file) in
+    L.set_lexer_state !state;
+    let a = parsable c in
+    state := L.release_lexer_state ();
+    (a,state)
   let action = Gramext.action
   let entry_create = Entry.create
   let entry_parse e (p,state) =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let c = Entry.parse e p in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       c
     with Exc_located (loc,e) ->
-      L.restore_comments_state L.default_comments_state;
+      L.drop_lexer_state ();
       let loc' = Loc.get_loc (Exninfo.info e) in
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
       Loc.raise ~loc e
   let with_parsable (p,state) f x =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let a = f x in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       a
     with e ->
-      L.restore_comments_state L.default_comments_state;
+      L.drop_lexer_state ();
       raise e
 
   let entry_print ft x = Entry.print ft x
@@ -234,7 +242,7 @@ module type GrammarSig = sig
   type 'a entry = 'a Entry.t
   type action = Action.t
   type coq_parsable
-  val parsable : char Stream.t -> coq_parsable
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -249,31 +257,28 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   include Camlp4.Struct.Grammar.Static.Make (L)
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type comments_state = int option * string * bool * ((int * int) * string) list
-  type coq_parsable = char Stream.t * L.comments_state ref
-  let parsable s = let state = ref L.default_comments_state in (s, state)
+  type coq_parsable = char Stream.t * L.lexer_state ref
+  let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state)
   let action = Action.mk
   let entry_create = Entry.mk
   let entry_parse e (s,state) =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let c = parse e (*FIXME*)CompatLoc.ghost s in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       c
     with Exc_located (loc,e) ->
-      L.restore_comments_state L.default_comments_state;
-      raise_coq_loc loc e
+      L.drop_lexer_state ();
+      raise_coq_loc loc e;;
   let with_parsable (p,state) f x =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let a = f x in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       a
     with e ->
-      L.restore_comments_state L.default_comments_state;
-      raise e
+      L.drop_lexer_state ();
+      Pervasives.raise e;;
   let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 51d006e255..3045d66b80 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -99,19 +99,19 @@ let position_problem l2r = function
   | CONV -> None
   | CUMUL -> Some l2r
 
-let occur_rigidly ev evd t = 
+let occur_rigidly (evk,_ as ev) evd t =
   let rec aux t =
     match kind_of_term (whd_evar evd t) with
     | App (f, c) -> if aux f then Array.exists aux c else false
     | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
     | Proj (p, c) -> not (aux c)
-    | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false
+    | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false
     | Cast (p, _, _) -> aux p
     | Lambda _ | LetIn _ -> false
     | Const _ -> false
     | Prod (_, b, t) -> ignore(aux b || aux t); true
     | Rel _ | Var _ -> false
-    | Case _ -> false
+    | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false
   in try ignore(aux t); false with Occur -> true
 
 (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
@@ -480,7 +480,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	      ise_try evd 
 	        [eta;(* Postpone the use of an heuristic *)
 		 (fun i -> 
-		   if not (occur_rigidly (fst ev) i tR) then
+		   if not (occur_rigidly ev i tR) then
                      let i,tF =
                        if isRel tR || isVar tR then
                          (* Optimization so as to generate candidates *)
@@ -1151,7 +1151,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
       Success (solve_refl ~can_drop:true f env evd
                  (position_problem true pbty) evk1 args1 args2)
-  | Evar ev1, Evar ev2 ->
+  | Evar ev1, Evar ev2 when app_empty ->
       Success (solve_evar_evar ~force:true
         (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
         (position_problem true pbty) ev1 ev2)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c44903e8c3..6e5ded1523 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -613,7 +613,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
  * substitution u1..uq.
  *)
 
+exception MorePreciseOccurCheckNeeeded
+
 let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+  if Evd.is_defined evd evk1 then
+      (* Some circularity somewhere (see e.g. #3209) *)
+      raise MorePreciseOccurCheckNeeeded;
+  let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in
   let evi1 = Evd.find_undefined evd evk1 in
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
@@ -1553,6 +1559,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         postpone_non_unique_projection env evd pbty ev sols rhs
     | NotEnoughInformationEvarEvar t ->
         add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
+    | MorePreciseOccurCheckNeeeded ->
+        add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
     | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
         raise e
     | OccurCheckIn (evd,rhs) ->
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index c94650f1ee..aa94fb7be3 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -129,7 +129,7 @@ end) = struct
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.extract_comments n)
+    if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
     else mt()
 
   let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 4916889139..50630fb9b5 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -15,7 +15,7 @@ open Locus
 open Genredexpr
 
 let pr_located pr (loc, x) =
-  if Flags.do_beautify () && loc <> Loc.ghost then
+  if !Flags.beautify && loc <> Loc.ghost then
     let (b, e) = Loc.unloc loc in
     (* Side-effect: order matters *)
     let before = Pp.comment (CLexer.extract_comments b) in
diff --git a/test-suite/bugs/closed/3209.v b/test-suite/bugs/closed/3209.v
new file mode 100644
index 0000000000..855058b011
--- /dev/null
+++ b/test-suite/bugs/closed/3209.v
@@ -0,0 +1,75 @@
+(* Avoiding some occur-check *)
+
+(* 1. Original example *)
+
+Inductive eqT {A} (x : A) : A -> Type :=
+  reflT : eqT x x.
+Definition Bi_inv (A B : Type) (f : (A -> B)) :=
+  sigT (fun (g : B -> A) =>
+          sigT (fun (h : B -> A) =>
+                  sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
+                          forall a : A, eqT (h (f a)) a))).
+Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).
+
+Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
+Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
+  sigT_rect (fun _ => TEquiv A B)
+            (fun (f : TEquiv A B -> eqT A B) H =>
+               sigT_rect _ (* (fun _ => TEquiv A B) *)
+                         (fun g _ => g e)
+                         H)
+            (UA A B).
+
+(* 2. Alternative example by Guillaume *)
+
+Inductive foo (A : Prop) : Prop := Foo : foo A.
+Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop.
+
+(* This used to fail with a Not_found, we fail more graciously but a
+   heuristic could be implemented, e.g. in some smart occur-check
+   function, to find a solution of then form ?P := fun _ => ?P' *)
+
+Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)).
+
+(* This works and tells which solution we could have inferred *)
+
+Check (fun e : ?[T] => bar ?[A] (fun _ => ?[P]) (fun g : ?[A'] => g e)).
+
+(* For the record, here is the trace in the failing example:
+
+In (fun e : ?T => bar ?[A] ?[P] (fun g : ?A' => g e)), we have the existential variables
+
+e:?T |- ?A : Prop
+e:?T |- ?P : foo ?A -> Prop
+e:?T |- ?A' : Type
+
+with constraints
+
+?A' == ?A
+?A' == ?T -> ?P (Foo ?A)
+
+To type (g e), unification first defines
+
+?A := forall x:?B, ?P'{e:=e,x:=x}
+with ?T <= ?B
+and ?P'@{e:=e,x:=e} <= ?P@{e:=e} (Foo (forall x:?B, ?P'{e:=e,x:=x}))
+
+Then, since ?P'@{e:=e,x:=e} may use "e" in two different ways, it is
+not a pattern and we define a new
+
+e:?T x:?B|- ?P'' : foo (?B' -> ?P''') -> Prop
+
+for some ?B' and ?P''', together with
+
+?P'@{e,x} := ?P''{e:=e,x:=e} (Foo (?B -> ?P')
+?P@{e} := ?P''{e:=e,x:=e}
+
+Moreover, ?B' and ?P''' have to satisfy
+
+?B'@{e:=e,x:=e} == ?B@{e:=e}
+?P'''@{e:=e,x:=e} == ?P'@{e:=e,x:=x}
+
+and this leads to define ?P' which was the initial existential
+variable to define.
+*)
+
diff --git a/test-suite/bugs/closed/4955.v b/test-suite/bugs/closed/4955.v
new file mode 100644
index 0000000000..dce1f764c3
--- /dev/null
+++ b/test-suite/bugs/closed/4955.v
@@ -0,0 +1,98 @@
+(* An example involving a first-order unification triggering a cyclic constraint *)
+
+Module A.
+Notation "{ x : A | P }" := (sigT (fun x:A => P)).
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation "p @ q" := (eq_trans p q) (at level 20).
+Notation "p ^" := (eq_sym p) (at level 3).
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) 
+: P y :=
+  match p with eq_refl => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only 
+parsing).
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with eq_refl => eq_refl end.
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): p # (f 
+x) = f y
+  := match p with eq_refl => eq_refl end.
+Axiom transport_compose
+  : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f 
+x)),
+    transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Delimit Scope functor_scope with functor.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) 
+(object_of d) }.
+Arguments object_of {C%category D%category} f%functor c%object : rename, simpl 
+nomatch.
+Arguments morphism_of [C%category] [D%category] f%functor [s%object d%object] 
+m%morphism : rename, simpl nomatch.
+Section path_functor.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Local Notation path_functor'_T F G
+    := { HO : object_of F = object_of G
+       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) 
+(GO d))
+                   HO
+                   (morphism_of F)
+         = morphism_of G }
+         (only parsing).
+  Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> 
+path_functor'_T F G
+    := fun H'
+       => (ap object_of H';
+             (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H').
+
+End path_functor.
+End A.
+
+(* A variant of it with more axioms *)
+
+Module B.
+Notation "{ x : A | P }" := (sigT (fun x:A => P)).
+Notation "( x ; y )" := (existT _ x y).
+Notation "p @ q" := (eq_trans p q) (at level 20).
+Notation "p ^" := (eq_sym p) (at level 3).
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only 
+parsing).
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with eq_refl => eq_refl end.
+Axiom apD : forall {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y), p # (f 
+x) = f y.
+Axiom transport_compose
+  : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f 
+x)),
+    transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) 
+(object_of d) }.
+Arguments object_of {C D} f c : rename, simpl nomatch.
+Arguments morphism_of [C] [D] f [s d] m : rename, simpl nomatch.
+Section path_functor.
+  Variable C D : PreCategory.
+  Local Notation path_functor'_T F G
+    := { HO : object_of F = object_of G
+       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) 
+(GO d))
+                   HO
+                   (morphism_of F)
+         = morphism_of G }.
+  Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> 
+path_functor'_T F G
+    := fun H'
+       => (ap object_of H';
+             (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H').
+
+End path_functor.
+End B.
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 5541ccf57b..ad60aeccce 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -60,3 +60,27 @@ exist (Q x) y conj
      : nat -> nat
 {1, 2}
      : nat -> Prop
+a#
+     : Set
+a#
+     : Set
+a≡
+     : Set
+a≡
+     : Set
+.≡
+     : Set
+.≡
+     : Set
+.a#
+     : Set
+.a#
+     : Set
+.a≡
+     : Set
+.a≡
+     : Set
+.α
+     : Set
+.α
+     : Set
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 1d8278c088..ceb29d1b9e 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -116,3 +116,32 @@ Check %j.
 
 Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
 Check ({1, 2}).
+
+(**********************************************************************)
+(* Check notations of the form ".a", ".a≡", "a≡"                      *)
+(* Only "a#", "a≡" and ".≡" were working properly for parsing. The    *)
+(* other ones were working only for printing.                         *)
+
+Notation "a#" := nat.
+Check nat.
+Check a#.
+
+Notation "a≡" := nat.
+Check nat.
+Check a≡.
+
+Notation ".≡" := nat.
+Check nat.
+Check .≡.
+
+Notation ".a#" := nat.
+Check nat.
+Check .a#.
+
+Notation ".a≡" := nat.
+Check nat.
+Check .a≡.
+
+Notation ".α" := nat.
+Check nat.
+Check .α.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 71e1f9593d..f0f8f18641 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -34,7 +34,7 @@ let resize_buffer ibuf =
   ibuf.str <- nstr
 
 (* Delete all irrelevant lines of the input buffer. Keep the last line
-   in the buffer (useful when there are several commands on the same line. *)
+   in the buffer (useful when there are several commands on the same line). *)
 
 let resynch_buffer ibuf =
   match ibuf.bols with
@@ -299,7 +299,7 @@ let do_vernac () =
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.eval_expr input (read_sentence input)
+    Vernac.process_expr top_buffer.tokens (read_sentence input)
   with
     | End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
@@ -308,7 +308,6 @@ let do_vernac () =
         else Feedback.msg_error (str"There is no ML toplevel.")
     | any ->
         let any = CErrors.push any in
-        Format.set_formatter_out_channel stdout;
         let msg = print_toplevel_error any ++ fnl () in
         pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
         Format.pp_print_flush !Pp_control.std_ft ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7a67e0951f..5ae1c36ed8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -168,7 +168,7 @@ let load_vernacular () =
   List.iter
     (fun (s,b) ->
       let s = Loadpath.locate_file s in
-      if Flags.do_beautify () then
+      if !Flags.beautify then
 	with_option beautify_file (Vernac.load_vernac b) s
       else
 	Vernac.load_vernac b s)
@@ -219,7 +219,7 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 
 let compile_file (v,f) =
-  if Flags.do_beautify () then
+  if !Flags.beautify then
     with_option beautify_file (Vernac.compile v) f
   else
     Vernac.compile v f
@@ -228,11 +228,9 @@ let compile_files () =
   if !compile_list == [] then ()
   else
     let init_state = States.freeze ~marshallable:`No in
-    let coqdoc_init_state = CLexer.location_table () in
     Feedback.(add_feeder debug_feeder);
     List.iter (fun vf ->
         States.unfreeze init_state;
-        CLexer.restore_location_table coqdoc_init_state;
         compile_file vf)
       (List.rev !compile_list)
 
@@ -538,7 +536,7 @@ let parse_args arglist =
         Flags.async_proofs_never_reopen_branch := true;
     |"-batch" -> set_batch_mode ()
     |"-test-mode" -> test_mode := true
-    |"-beautify" -> make_beautify true
+    |"-beautify" -> beautify := true
     |"-boot" -> boot := true; no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
     |"-color" -> set_color (next ())
@@ -550,7 +548,7 @@ let parse_args arglist =
     |"-ideslave" -> set_ideslave ()
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
-    |"-just-parsing" -> Vernac.just_parsing := true
+    |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6"
     |"-m"|"--memory" -> memory_stat := true
     |"-noinit"|"-nois" -> load_init := false
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a37859c9ca..74adf497e3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -18,6 +18,8 @@ open Vernacexpr
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
+let user_error loc s = CErrors.user_err ~loc (str s)
+
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
 
 let rec is_navigation_vernac = function
@@ -42,6 +44,14 @@ let is_reset = function
   | VernacResetInitial | VernacResetName _ -> true
   | _ -> false
 
+let checknav_simple loc cmd =
+  if is_navigation_vernac cmd && not (is_reset cmd) then
+    user_error loc "Navigation commands forbidden in files."
+
+let checknav_deep loc ast =
+  if is_deep_navigation_vernac ast then
+    user_error loc "Navigation commands forbidden in nested commands."
+
 (* When doing Load on a file, two behaviors are possible:
 
    - either the history stack is grown by only one command,
@@ -70,8 +80,6 @@ let disable_drop = function
   | Drop -> CErrors.error "Drop is forbidden."
   | e -> e
 
-let user_error loc s = CErrors.user_err ~loc ~hdr:"_" (str s)
-
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
@@ -81,7 +89,7 @@ let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
-  let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
+  let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
   (in_chan, longfname, (po, verb_ch))
 
 let close_input in_chan (_,verb) =
@@ -114,48 +122,39 @@ let parse_sentence = Flags.with_option Flags.we_are_parsing
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
-let just_parsing = ref false
 let chan_beautify = ref stdout
 let beautify_suffix = ".beautified"
 
-let set_formatter_translator() =
-  let ch = !chan_beautify in
+let set_formatter_translator ch =
   let out s b e = output ch s b e in
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
-let pr_new_syntax_in_context loc ocom =
+let pr_new_syntax_in_context loc chan_beautify ocom =
   let loc = Loc.unloc loc in
-  if !beautify_file then set_formatter_translator();
+  if !beautify_file then set_formatter_translator chan_beautify;
   let fs = States.freeze ~marshallable:`No in
-  (* Side-effect: order matters *)
-  let before = comment (CLexer.extract_comments (fst loc)) in
-  let com = match ocom with
-    | Some com -> Ppvernac.pr_vernac com
-    | None -> mt() in
-  let after = comment (CLexer.extract_comments (snd loc)) in
-  if !beautify_file then
-    Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
-  else
-    Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
-  States.unfreeze fs;
-  Format.set_formatter_out_channel stdout
-
-let pr_new_syntax (po,_) loc ocom =
-  (* Reinstall the context of parsing which includes the bindings of comments to locations *)
-  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom
-
-let save_translator_coqdoc () =
-  (* translator state *)
-  let ch = !chan_beautify in
-  (* end translator state *)
-  let coqdocstate = CLexer.location_table () in
-  ch,coqdocstate
+  (* The content of this is not supposed to fail, but if ever *)
+  try
+    (* Side-effect: order matters *)
+    let before = comment (CLexer.extract_comments (fst loc)) in
+    let com = match ocom with
+      | Some com -> Ppvernac.pr_vernac com
+      | None -> mt() in
+    let after = comment (CLexer.extract_comments (snd loc)) in
+    if !beautify_file then
+      Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
+    else
+      Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+    States.unfreeze fs;
+    Format.set_formatter_out_channel stdout
+  with any ->
+    States.unfreeze fs;
+    Format.set_formatter_out_channel stdout
 
-let restore_translator_coqdoc (ch,coqdocstate) =
-  if !Flags.beautify_file then close_out !chan_beautify;
-  chan_beautify := ch;
-  CLexer.restore_location_table coqdocstate
+let pr_new_syntax po loc chan_beautify ocom =
+  (* Reinstall the context of parsing which includes the bindings of comments to locations *)
+  Pcoq.Gram.with_parsable po (pr_new_syntax_in_context chan_beautify loc) ocom
 
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
@@ -185,72 +184,52 @@ let print_cmd_header loc com =
   Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Pp_control.std_ft ()
 
-let rec vernac_com input checknav (loc,com) =
+let rec interp_vernac po chan_beautify checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-	let st = save_translator_coqdoc () in
-        let old_lexer_file = CLexer.get_current_file () in
-        CLexer.set_current_file f;
-	if !Flags.beautify_file then
-	  begin
-	    chan_beautify := open_out (f^beautify_suffix);
-          end;
-	begin
-	  try
-            Flags.silently (read_vernac_file verbosely) f;
-	    restore_translator_coqdoc st;
-            CLexer.set_current_file old_lexer_file;
-	  with reraise ->
-            let reraise = CErrors.push reraise in
-	    restore_translator_coqdoc st;
-            CLexer.set_current_file old_lexer_file;
-	    iraise reraise
-	end
-
-    | v when !just_parsing -> ()
+        load_vernac verbosely f
 
     | v -> Stm.interp (Flags.is_verbose()) (loc,v)
   in
     try
       checknav loc com;
-      if do_beautify () then pr_new_syntax input loc (Some com);
+      if !beautify then pr_new_syntax po chan_beautify loc (Some com);
       (* XXX: This is not 100% correct if called from an IDE context *)
       if !Flags.time then print_cmd_header loc com;
       let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
       let (reraise, info) = CErrors.push reraise in
-      Format.set_formatter_out_channel stdout;
       let loc' = Option.default Loc.ghost (Loc.get_loc info) in
       if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
       else iraise (reraise, info)
 
-and read_vernac_file verbosely s =
-  let checknav loc cmd =
-    if is_navigation_vernac cmd && not (is_reset cmd) then
-	user_error loc "Navigation commands forbidden in files"
-  in
-  let (in_chan, fname, input) = open_file_twice_if verbosely s in
+(* Load a vernac file. CErrors are annotated with file and location *)
+and load_vernac verbosely file =
+  let chan_beautify =
+    if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in
+  let (in_chan, fname, input) = open_file_twice_if verbosely file in
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
     while true do
-      let loc_ast = parse_sentence input in
+      let loc_ast = Flags.silently parse_sentence input in
       CWarnings.set_current_loc (fst loc_ast);
-      vernac_com input checknav loc_ast;
+      Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast;
     done
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
-    Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
-          if do_beautify () then
-            pr_new_syntax input (Loc.make_loc (max_int,max_int)) None
+          if !beautify then
+            pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None;
+          if !Flags.beautify_file then close_out chan_beautify;
       | reraise ->
+         if !Flags.beautify_file then close_out chan_beautify;
 	 iraise (disable_drop e, info)
 
 (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
@@ -260,32 +239,12 @@ and read_vernac_file verbosely s =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let checknav loc ast =
-  if is_deep_navigation_vernac ast then
-    user_error loc "Navigation commands forbidden in nested commands"
-
-let eval_expr input loc_ast = vernac_com input checknav loc_ast
+let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
 let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
 
-(* Load a vernac file. CErrors are annotated with file and location *)
-let load_vernac verb file =
-  chan_beautify :=
-    if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
-    let old_lexer_file = CLexer.get_current_file () in
-  try
-    CLexer.set_current_file file;
-    Flags.silently (read_vernac_file verb) file;
-    if !Flags.beautify_file then close_out !chan_beautify;
-    CLexer.set_current_file old_lexer_file;
-  with any ->
-    let (e, info) = CErrors.push any in
-    if !Flags.beautify_file then close_out !chan_beautify;
-    CLexer.set_current_file old_lexer_file;
-    iraise (disable_drop e, info)
-
 let warn_file_no_extension =
   CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
          (fun (f,ext) ->
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 2fd86ddc22..0d9f5871a3 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -14,14 +14,11 @@
 val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
  Loc.t * Vernacexpr.vernac_expr
 
-(** Reads and executes vernac commands from a stream.
-   The boolean [just_parsing] disables interpretation of commands. *)
+(** Reads and executes vernac commands from a stream. *)
 
 exception End_of_input
 
-val just_parsing : bool ref
-
-val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit
+val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit
 
 (** Set XML hooks *)
 val xml_start_library : (unit -> unit) Hook.t
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 607bb6cfb4..4000a1d34d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1814,7 +1814,7 @@ let vernac_load interp fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
-    Pcoq.Gram.parsable (Stream.of_channel in_chan) in
+    Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()