From 1fda29d0179d60c83ead5db6e3062511aba7d264 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 19 Sep 2016 17:53:43 +0200
Subject: Fix warning when using Variables at toplevel.

---
 toplevel/command.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 097865648e..12c387dcf3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -140,21 +140,21 @@ let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
   ce
 
-let warn_local_let_definition =
-  CWarnings.create ~name:"local-let-definition" ~category:"scope"
-         (fun id ->
-          pr_id id ++ strbrk " is declared as a local definition")
+let warn_local_declaration =
+  CWarnings.create ~name:"local-declaration" ~category:"scope"
+         (fun (id,kind) ->
+          pr_id id ++ strbrk " is declared as a local " ++ str kind)
 
-let get_locality id = function
+let get_locality id ~kind = function
 | Discharge ->
   (** If a Let is defined outside a section, then we consider it as a local definition *)
-   warn_local_let_definition id;
+   warn_local_declaration (id,kind);
   true
 | Local -> true
 | Global -> false
 
 let declare_global_definition ident ce local k pl imps =
-  let local = get_locality ident local in
+  let local = get_locality ident ~kind:"definition" local in
   let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -238,7 +238,7 @@ match local with
   (r,Univ.Instance.empty,true)
 
 | Global | Local | Discharge ->
-  let local = get_locality ident local in
+  let local = get_locality ident ~kind:"axiom" local in
   let inl = match nl with
     | NoInline -> None
     | DefaultInline -> Some (Flags.get_inline_level())
-- 
cgit v1.2.3


From 20d6c289bff303ec1a4cab3a56431989d0e527d2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 22 Sep 2016 21:59:38 +0200
Subject: coqc -o now places .glob file near .vo file

All compilation (by)products are placed where -o specifies.
Used to be the case for .vo, .vio, .aux but not .glob
---
 toplevel/vernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index de3d144838..55f3a31a34 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -345,7 +345,7 @@ let compile verbosely f =
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_vo)
         ~v_file:long_f_dot_v);
-      Dumpglob.start_dump_glob long_f_dot_v;
+      Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       if !Flags.xml_export then Hook.get f_xml_start_library ();
       let wall_clock1 = Unix.gettimeofday () in
-- 
cgit v1.2.3