From d65eaaaa8cb311a0344a584df7a4b405034780b9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Mar 2015 15:56:51 +0100
Subject: Revert "Useless check when loading notations through import."

This reverts commit 124734fd2c523909802d095abb37350519856864.
---
 toplevel/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cdbff17149..c8eff59b15 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1118,7 +1118,7 @@ let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
-  if Int.equal i 1 then begin
+  if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
     (* Declare the interpretation *)
     Notation.declare_notation_interpretation ntn scope pat df;
     (* Declare the uninterpretation *)
-- 
cgit v1.2.3


From 57109109a53c4bbbd7c8fa0acc142e47c80c5df7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Mar 2015 11:09:56 +0100
Subject: coqc: fix --help

---
 toplevel/usage.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 6909d89440..4ee3bc4745 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -48,6 +48,10 @@ let print_usage_channel co command =
 \n  -compile f             compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
 \n  -quick                 quickly compile .v files to .vio files (skip proofs)\
+\n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
+\n                         into fi.vo\
+\n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
+\n                         proofs in each fi.vio\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config                print Coq's configuration information and exit\
-- 
cgit v1.2.3


From e8b4756c655eacd8a2b9b23630ba02dbbbc4e96e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Mar 2015 18:17:03 +0100
Subject: Putting the From parameter of the Require command into the AST.

---
 toplevel/vernacentries.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a4ffae0fff..62e5f0a324 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -749,7 +749,11 @@ let vernac_end_segment (_,id as lid) =
 
 (* Libraries *)
 
-let vernac_require import qidl =
+let vernac_require from import qidl =
+  let qidl = match from with
+  | None -> qidl
+  | Some ns -> List.map (Libnames.join_reference ns) qidl
+  in
   let qidl = List.map qualid_of_reference qidl in
   let modrefl = List.map Library.try_locate_qualified_library qidl in
   if Dumpglob.dump () then
@@ -1884,7 +1888,7 @@ let interp ?proof locality poly c =
 
   | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set
 
-  | VernacRequire (export, qidl) -> vernac_require export qidl
+  | VernacRequire (from, export, qidl) -> vernac_require from export qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
   | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t
-- 
cgit v1.2.3