Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

8 files changed, 69 insertions, 24 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 96bb89e2a4..f905080905 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -355,7 +355,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
       )
   in
   Proofview.Goal.nf_enter begin fun gl ->
-    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in
+    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
@@ -417,7 +417,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
         Proofview.Goal.enter begin fun gl ->
-        let tt1 = Tacmach.New.pf_type_of gl t1 in
+        let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind tt1
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6a485d52c0..0e270f960b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly =
   let _ =
     if not
       (Reductionops.is_conv_leq env Evd.empty
-	(Typing.type_of env Evd.empty val_f) typ_f)
+	(Typing.unsafe_type_of env Evd.empty val_f) typ_f)
     then
       errorlabstrm "" (strbrk
 	"Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1249581eec..7cf0477f9f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -847,7 +847,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
   let () = check_evars_are_solved env !evdref (Evd.empty,!evdref)  in
-  let relty = Typing.type_of env !evdref rel in
+  let relty = Typing.unsafe_type_of env !evdref rel in
   let relargty =
     let error () =
       user_err_loc (constr_loc r,
@@ -988,7 +988,7 @@ let interp_recursive isfix fixl notations =
     List.fold_left2
       (fun env' id t ->
 	 if Flags.is_program_mode () then
-	   let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in
+	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
 	   let fixprot =
 	     try 
 	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ca379cb7e7..56b5442922 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -114,6 +114,11 @@ let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
 
 let set_batch_mode () = batch_mode := true
 
+let set_warning = function
+| "all" -> make_warn true
+| "none" -> make_warn false
+| _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
+
 let toplevel_default_name = DirPath.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
@@ -276,7 +281,16 @@ let print_style_tags () =
     in
     print_string opt
   in
-  List.iter iter tags;
+  let make (t, st) = match st with
+  | None -> None
+  | Some st ->
+    let tags = List.map string_of_int (Terminal.repr st) in
+    let t = String.concat "." (Ppstyle.repr t) in
+    Some (t ^ "=" ^ String.concat ";" tags)
+  in
+  let repr = List.map_filter make tags in
+  let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in
+  let () = List.iter iter tags in
   flush_all ()
 
 let error_missing_arg s =
@@ -472,6 +486,7 @@ let parse_args arglist =
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> toploop := Some (next ())
+    |"-w" -> set_warning (next ())
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
@@ -498,11 +513,14 @@ let parse_args arglist =
     |"-noinit"|"-nois" -> load_init := false
     |"-no-compat-notations" -> no_compat_ntn := true
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
-    |"-no-native-compiler" -> no_native_compiler := true
+    |"-native-compiler" ->
+      if Coq_config.no_native_compiler then
+	warning "Native compilation was disabled at configure time."
+      else native_compiler := true
     |"-notop" -> unset_toplevel_name ()
     |"-output-context" -> output_context := true
     |"-q" -> no_load_rc ()
-    |"-quiet"|"-silent" -> Flags.make_silent true
+    |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false
     |"-quick" -> Flags.compilation_mode := BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index deffb4fe51..98b322af1d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -84,8 +84,14 @@ type tactic_grammar_obj = {
   tacobj_body : Tacexpr.glob_tactic_expr
 }
 
+let check_key key =
+  if Tacenv.check_alias key then
+    error "Conflicting tactic notations keys. This can happen when including \
+    twice the same module."
+
 let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
+  let () = check_key key in
   Tacenv.register_alias key tobj.tacobj_body;
   Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
@@ -97,6 +103,7 @@ let open_tactic_notation i (_, tobj) =
 
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
+  let () = check_key key in
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f053839c70..50fb019f47 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -56,6 +56,10 @@ let print_usage_channel co command =
 \n  -v                     print Coq version and exit\
 \n  -list-tags             print highlight color tags known by Coq and exit\
 \n\
+\n  -quiet                 unset display of extra information (implies -w none)\
+\n  -w (all|none)          configure display of warnings\
+\n  -color (on|off|auto)   configure color output (only active through coqtop)\
+\n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
 \n  -batch                 batch mode (exits just after arguments parsing)\
@@ -63,7 +67,6 @@ let print_usage_channel co command =
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
 \n  -emacs                 tells Coq it is executed under Emacs\
-\n  -color (on|off|auto)   configure color output (only active through coqtop)\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
@@ -71,7 +74,7 @@ let print_usage_channel co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -time                  display the time taken by each command\
-\n  -no-native-compiler    disable the native_compute reduction machinery\
+\n  -native-compiler       precompile files for the native_compute machinery\
 \n  -h, -help              print this list of options\
 \n";
   List.iter (fun (name, text) ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 11cb047e09..5418c60e94 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -78,9 +78,13 @@ let get_exn_files e = Exninfo.get e files_of_exn
 
 let add_exn_files e f = Exninfo.add e files_of_exn f
 
-let raise_with_file f (e, info) =
-  let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in
-  iraise (e, add_exn_files info { outer = f; inner = inner_f })
+let enrich_with_file f (e, info) =
+  let inner = match get_exn_files info with None -> f | Some x -> x.inner in
+  (e, add_exn_files info { outer = f; inner })
+
+let raise_with_file f e = iraise (enrich_with_file f e)
+
+let cur_file = ref None
 
 let disable_drop = function
   | Drop -> Errors.error "Drop is forbidden."
@@ -253,13 +257,12 @@ let rec vernac_com verbosely checknav (loc,com) =
       else iraise (reraise, info)
 
 and read_vernac_file verbosely s =
-  Flags.make_warn verbosely;
   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
+  let (in_chan, fname, input) = open_file_twice_if verbosely s in
+  cur_file := Some fname;
   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 *)
@@ -350,3 +353,8 @@ let compile v f =
   compile v f;
   CoqworkmgrApi.giveback 1
 
+let () = Hook.set Stm.process_error_hook (fun e ->
+  match !cur_file with
+  | None -> Cerrors.process_vernac_interp_error e
+  | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e)
+)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4300d5e244..9d5edc80a0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -379,17 +379,27 @@ let msg_found_library = function
       msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
 
-let err_unmapped_library loc qid =
+let err_unmapped_library loc ?from qid =
   let dir = fst (repr_qualid qid) in
+  let prefix = match from with
+  | None -> str "."
+  | Some from ->
+    str " and prefix " ++ pr_dirpath from ++ str "."
+  in
   user_err_loc
     (loc,"locate_library",
-     strbrk "Cannot find a physical path bound to logical path " ++
-       pr_dirpath dir ++ str".")
+     strbrk "Cannot find a physical path bound to logical path matching suffix " ++
+       pr_dirpath dir ++ prefix)
 
-let err_notfound_library loc qid =
+let err_notfound_library loc ?from qid =
+  let prefix = match from with
+  | None -> str "."
+  | Some from ->
+    str " with prefix " ++ pr_dirpath from ++ str "."
+  in
   user_err_loc
     (loc,"locate_library",
-     strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")
+     strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
 
 let print_located_library r =
   let (loc,qid) = qualid_of_reference r in
@@ -759,8 +769,8 @@ let vernac_require from import qidl =
       let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
       (dir, f)
     with
-      | Library.LibUnmappedDir -> err_unmapped_library loc qid
-      | Library.LibNotFound -> err_notfound_library loc qid
+      | Library.LibUnmappedDir -> err_unmapped_library loc ?from:root qid
+      | Library.LibNotFound -> err_notfound_library loc ?from:root qid
   in
   let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
@@ -2164,5 +2174,4 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     else aux false c
 
 let () = Hook.set Stm.interp_hook interp
-let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error
 let () = Hook.set Stm.with_fail_hook with_fail