Merge branch 'v8.5'

6 files changed, 23 insertions, 21 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 4f3ffbcaee..0bb7966d72 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -35,7 +35,7 @@ let explain_exn_default = function
   (* Basic interaction exceptions *)
   | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
-  | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
+  | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err))
   | Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
   | Out_of_memory -> hov 0 (str "Out of memory.")
   | Stack_overflow -> hov 0 (str "Stack overflow.")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 063ed89643..040c339249 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -288,7 +288,7 @@ let rec discard_to_dot () =
   try
     Gram.entry_parse parse_to_dot top_buffer.tokens
   with
-    | Compat.Token.Error _ | Lexer.Error.E _ -> discard_to_dot ()
+    | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
     | End_of_input -> raise End_of_input
     | e when Errors.noncritical e -> ()
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c6f49dcd48..c4222b3305 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -229,11 +229,11 @@ let compile_files () =
     | [vf] -> compile_file vf (* One compilation : no need to save init state *)
     | l ->
       let init_state = States.freeze ~marshallable:`No in
-      let coqdoc_init_state = Lexer.location_table () in
+      let coqdoc_init_state = CLexer.location_table () in
       List.iter
         (fun vf ->
 	  States.unfreeze init_state;
-	  Lexer.restore_location_table coqdoc_init_state;
+	  CLexer.restore_location_table coqdoc_init_state;
           compile_file vf)
         (List.rev l)
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 701bc5da54..d60c739399 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -30,7 +30,7 @@ open Nameops
 (**********************************************************************)
 (* Tokens                                                             *)
 
-let cache_token (_,s) = Lexer.add_keyword s
+let cache_token (_,s) = CLexer.add_keyword s
 
 let inToken : string -> obj =
   declare_object {(default_object "TOKEN") with
@@ -272,7 +272,7 @@ let rec interp_list_parser hd = function
 (* To protect alphabetic tokens and quotes from being seen as variables *)
 let quote_notation_token x =
   let n = String.length x in
-  let norm = Lexer.is_ident x in
+  let norm = CLexer.is_ident x in
   if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
   else x
 
@@ -280,7 +280,7 @@ let rec raw_analyze_notation_tokens = function
   | []    -> []
   | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
   | String "_" :: _ -> error "_ must be quoted."
-  | String x :: sl when Lexer.is_ident x ->
+  | String x :: sl when CLexer.is_ident x ->
       NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
       Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
@@ -569,7 +569,7 @@ let rec define_keywords_aux = function
   | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
       when is_not_small_constr e ->
       Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
-      Lexer.add_keyword k;
+      CLexer.add_keyword k;
       n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
   | [] -> []
@@ -578,7 +578,7 @@ let rec define_keywords_aux = function
 let define_keywords = function
   | GramConstrTerminal(IDENT k)::l ->
       Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
-      Lexer.add_keyword k;
+      CLexer.add_keyword k;
       GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
 
@@ -607,12 +607,12 @@ let make_production etyps symbols =
 	    let typ = List.assoc m etyps in
 	    distribute [GramConstrNonTerminal (typ, Some m)] ll
         | Terminal s ->
-	    distribute [GramConstrTerminal (Lexer.terminal s)] ll
+	    distribute [GramConstrTerminal (CLexer.terminal s)] ll
         | Break _ ->
             ll
         | SProdList (x,sl) ->
             let tkl = List.flatten
-              (List.map (function Terminal s -> [Lexer.terminal s]
+              (List.map (function Terminal s -> [CLexer.terminal s]
                 | Break _ -> []
                 | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in
 	    match List.assoc x etyps with
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b2fc456d07..54baa5e3c1 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -448,7 +448,7 @@ let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
     { obl with obl_type = t' }
 
-module ProgMap = Map.Make(Id)
+module ProgMap = Id.Map
 
 let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
 
@@ -698,11 +698,13 @@ let get_prog name =
 	     match n with
 		 0 -> raise (NoObligations None)
 	       | 1 -> get_info (map_first prg_infos)
-	       | _ -> 
-                   error ("More than one program with unsolved obligations: "^
-                    String.concat ", " 
-                     (List.map string_of_id
-                      (ProgMap.fold (fun k _ s -> k::s) prg_infos []))))
+	       | _ ->
+                let progs = Id.Set.elements (ProgMap.domain prg_infos) in
+                let prog = List.hd progs in
+                let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
+                errorlabstrm ""
+                  (str "More than one program with unsolved obligations: " ++ progs
+                  ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
 
 let get_any_prog () =
   let prg_infos = !from_prg in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1c8d602517..64225a644f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -162,17 +162,17 @@ let save_translator_coqdoc () =
   (* translator state *)
   let ch = !chan_beautify in
   let cl = !Pp.comments in
-  let cs = Lexer.com_state() in
+  let cs = CLexer.com_state() in
   (* end translator state *)
-  let coqdocstate = Lexer.location_table () in
+  let coqdocstate = CLexer.location_table () in
   ch,cl,cs,coqdocstate
 
 let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
   if !Flags.beautify_file then close_out !chan_beautify;
   chan_beautify := ch;
   Pp.comments := cl;
-  Lexer.restore_com_state cs;
-  Lexer.restore_location_table coqdocstate
+  CLexer.restore_com_state cs;
+  CLexer.restore_location_table coqdocstate
 
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)