From 102d2db3ea7a7354de5e019224e2778fe7603b8e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 21 Nov 2016 07:25:30 +0100
Subject: Stop parsing -compat-notations options, which are no longer supported
 (bug #3339).

---
 tools/coqc.ml     | 1 -
 toplevel/usage.ml | 2 --
 2 files changed, 3 deletions(-)

diff --git a/tools/coqc.ml b/tools/coqc.ml
index b59bbdb1e0..b12d48710f 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -94,7 +94,6 @@ let parse_args () =
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
       |"-impredicative-set"|"-vm"|"-native-compiler"
-      |"-verbose-compat-notations"|"-no-compat-notations"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       as o) :: rem ->
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 956a402617..38ceacf5ec 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -36,8 +36,6 @@ let print_usage_channel co command =
 \n  -noinit                start without loading the Init library\
 \n  -nois                  (idem)\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
-\n  -verbose-compat-notations  be warned when using compatibility notations\
-\n  -no-compat-notations   get an error when using compatibility notations\
 \n\
 \n  -load-ml-object f      load ML object file f\
 \n  -load-ml-source f      load ML file f\
-- 
cgit v1.2.3


From aa86963464045d61fa0eaf3a7fe67ced7a6a73f4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 21 Nov 2016 12:49:17 +0100
Subject: Remove spurious spaces in merlin file generated by coq_makefile (bug
 #5213).

---
 tools/coq_makefile.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ac69a69a4a..eab909f5b1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -887,7 +887,7 @@ let merlin targets (ml_inc,_,_) =
   print ".merlin:\n";
   print "\t@echo 'FLG -rectypes' > .merlin\n" ;
   List.iter (fun c ->
-      printf "\t@echo \"B $(COQLIB) %s\" >> .merlin\n" c)
+      printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
     lib_dirs ;
   List.iter (fun (_,c) ->
       printf "\t@echo \"B %s\" >> .merlin\n" c;
-- 
cgit v1.2.3


From a277da239514ad3bcabc7933a14cfcdc46f272e5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 10:54:20 +0100
Subject: Properly parenthesize "ltac:" arguments (bug #5169).

---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 1e618b59eb..6e40e03f5b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1216,7 +1216,7 @@ module Make
           | TacNumgoals ->
             keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-            keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
+            str "ltac:(" ++ pr_tac (1,Any) (TacArg (Loc.ghost,a)) ++ str ")"
 
         in pr_tac
 
-- 
cgit v1.2.3


From 989553966c7ba1a2cc23fd10fc2633dcb0f98648 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 10:03:17 +0100
Subject: Fix incorrect long multiplication in the VM.

If the result had its 30th bit set, then all the high part of the result
on a 64-bit architecture would end up being set, thus breaking subsequent
computations.

This patch also fixes the incorrectly parenthesized definition of
uint32_of_value, which by luck was never misused.
---
 kernel/byterun/coq_interp.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 792a311fcf..47df22807f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -23,7 +23,7 @@
 #include "coq_values.h" 
 
 /* spiwack: I append here a few macros for value/number manipulation */
-#define uint32_of_value(val) (((uint32_t)val >> 1))
+#define uint32_of_value(val) ((uint32_t)(val) >> 1)
 #define value_of_uint32(i)   ((value)(((uint32_t)(i) << 1) | 1))
 #define UI64_of_uint32(lo) ((uint64_t)(lo))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
@@ -1206,7 +1206,7 @@ value coq_interprete
 	  Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
 	  /*unsigned shift*/
 	  Field(accu, 0) = (value)((p >> 31)|1) ;  /*higher part*/
-	  Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/
+	  Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/
 	}
 	Next;
       }
-- 
cgit v1.2.3


From 9ddae1778aef70c55a1347c4d0b28694cf34a5af Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 13:39:06 +0100
Subject: Fix some documentation typos.

---
 ide/utils/configwin_keys.ml      | 2 +-
 parsing/pcoq.mli                 | 8 ++++----
 theories/Numbers/BigNumPrelude.v | 4 ++--
 theories/Strings/Ascii.v         | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml
index 9f44e5c6be..e9b19da621 100644
--- a/ide/utils/configwin_keys.ml
+++ b/ide/utils/configwin_keys.ml
@@ -154,7 +154,7 @@ let xk_KP_9			= 0xFFB9
 
 
 (*
- * Auxilliary Functions; note the duplicate definitions for left and right
+ * Auxiliary Functions; note the duplicate definitions for left and right
  * function keys;  Sun keyboards and a few other manufactures have such
  * function key groups on the left and/or right sides of the keyboard.
  * We've not found a keyboard with more than 35 function keys total.
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ec8dac8210..37165f6ceb 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -39,7 +39,7 @@ module Gram : module type of Compat.GrammarMake(CLexer)
         |     (together with a constr entry level, e.g. 50, and indications of)
         |     (subentries, e.g. x in constr next level and y constr same level)
         |
-        | spliting into tokens by Metasyntax.split_notation_string
+        | splitting into tokens by Metasyntax.split_notation_string
         V
       [String "x"; String "+"; String "y"] : symbol_token list
         |
@@ -96,7 +96,7 @@ module Gram : module type of Compat.GrammarMake(CLexer)
 
 *)
 
-(** Temporary activate camlp4 verbosity *)
+(** Temporarily activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
@@ -232,14 +232,14 @@ type gram_reinit = gram_assoc * gram_position
 
 val grammar_extend : 'a Gram.entry -> gram_reinit option ->
   'a Extend.extend_statment -> unit
-(** Extend the grammar of Coq, without synchronizing it with the bactracking
+(** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
 
 (** {5 Extending the parser with summary-synchronized commands} *)
 
 module GramState : Store.S
-(** Auxilliary state of the grammar. Any added data must be marshallable. *)
+(** Auxiliary state of the grammar. Any added data must be marshallable. *)
 
 type 'a grammar_command
 (** Type of synchronized parsing extensions. The ['a] type should be
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 45a7527c97..bd8930872c 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -10,7 +10,7 @@
 
 (** * BigNumPrelude *)
 
-(** Auxillary functions & theorems used for arbitrary precision efficient
+(** Auxiliary functions & theorems used for arbitrary precision efficient
     numbers. *)
 
 
@@ -22,7 +22,7 @@ Require Export Zpow_facts.
 Declare ML Module "numbers_syntax_plugin".
 
 (* *** Nota Bene ***
-   All results that were general enough has been moved in ZArith.
+   All results that were general enough have been moved in ZArith.
    Only remain here specialized lemmas and compatibility elements.
    (P.L. 5/11/2007).
 *)
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 97cb746f37..55a533c55a 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -40,7 +40,7 @@ Defined.
 
 (** * Conversion between natural numbers modulo 256 and ascii characters *)
 
-(** Auxillary function that turns a positive into an ascii by
+(** Auxiliary function that turns a positive into an ascii by
    looking at the last 8 bits, ie z mod 2^8 *)
 
 Definition ascii_of_pos : positive -> ascii :=
-- 
cgit v1.2.3


From b16de62d20790930589795c3d10fbb07185ec22c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 14:02:41 +0100
Subject: Lazily load constants in micromega (bug #5134).

---
 plugins/micromega/coq_micromega.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a063cbbfe3..e4b58a56f9 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1517,27 +1517,27 @@ let rec apply_ids t ids =
   | [] -> t
   | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
 
-let coq_Node = 
+let coq_Node = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
-let coq_Leaf = 
+let coq_Leaf = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
-let coq_Empty = 
+let coq_Empty = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
 
-let coq_VarMap = 
+let coq_VarMap = lazy
   (Coqlib.gen_constant_in_modules "VarMap"
      [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
  
 
 let rec dump_varmap typ m =
   match m with
-  | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |])
-  | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|])
-  | Mc.Node(l,o,r) -> 
-    Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+  | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |])
+  | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+  | Mc.Node(l,o,r) ->
+    Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
 
 
 let vm_of_list env =
@@ -1709,7 +1709,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
     (set
       [
        ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-       ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); 
+       ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
        ("__wit", cert, cert_typ)
       ]
       (Tacmach.pf_concl gl))
-- 
cgit v1.2.3


From a27ac0315dcbb99c64a260bac3988199a26b39cf Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 15:14:19 +0100
Subject: Fix some documentation typos.

Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
---
 CHANGES                       | 4 ++--
 config/coq_config.mli         | 4 ++--
 dev/doc/notes-on-conversion   | 2 +-
 doc/faq/FAQ.tex               | 4 ++--
 lib/profile.ml                | 6 +++---
 proofs/proof_global.ml        | 2 +-
 theories/FSets/FMapList.v     | 2 +-
 theories/FSets/FMapWeakList.v | 2 +-
 theories/FSets/FSetList.v     | 2 +-
 theories/FSets/FSetWeakList.v | 2 +-
 theories/MSets/MSetList.v     | 2 +-
 theories/MSets/MSetWeakList.v | 2 +-
 toplevel/vernacentries.ml     | 4 ++--
 13 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/CHANGES b/CHANGES
index 984e91946b..ecbf82e69d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1130,7 +1130,7 @@ Extraction
   instead of accessing their body, they are now considered as axioms.
   The previous behaviour can be reactivated via the option
   "Set Extraction AccessOpaque".
-- The pretty-printer for Haskell now produces layout-independant code
+- The pretty-printer for Haskell now produces layout-independent code
 - A new command "Separate Extraction cst1 cst2 ..." that mixes a
   minimal extracted environment a la "Recursive Extraction" and the
   production of several files (one per coq source) a la "Extraction Library"
@@ -1815,7 +1815,7 @@ Tactics
   Moreover, romega now has a variant "romega with *" that can be also used
   on non-Z goals (nat, N, positive) via a call to a translation tactic named
   zify (its purpose is to Z-ify your goal...). This zify may also be used
-  independantly of romega.
+  independently of romega.
 - Tactic "remember" now supports an "in" clause to remember only selected
   occurrences of a term.
 - Tactic "pose proof" supports name overwriting in case of specialization of an
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 6087c01169..c171bd3553 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -32,7 +32,7 @@ val cflags : string     (* arguments passed to gcc *)
 val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val arch_is_win32 : bool
-val osdeplibs : string  (* OS dependant link options for ocamlc *)
+val osdeplibs : string  (* OS dependent link options for ocamlc *)
 val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
 
 
@@ -51,7 +51,7 @@ val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
 val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
 
 val browser : string
-(** default web browser to use, may be overriden by environment
+(** default web browser to use, may be overridden by environment
     variable COQREMOTEBROWSER *)
 
 val has_coqide : string
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion
index 6274275c9d..a81f170c63 100644
--- a/dev/doc/notes-on-conversion
+++ b/dev/doc/notes-on-conversion
@@ -21,7 +21,7 @@ Notation OMEGA := (ack 4 4).
 
 Definition f (x:nat) := x.
 
-(* Evaluation in tactics can somehow be controled *)
+(* Evaluation in tactics can somehow be controlled *)
 Lemma l1 : OMEGA = OMEGA.
 reflexivity.  (* succeed: identity *)
 Qed.          (* succeed: identity *)
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 48b61827d1..213fb03137 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -2587,8 +2587,8 @@ It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots}
 
 \Question{What is a dependent type?}
 
-A dependant type is a type which depends on some term. For instance
-``vector of size n'' is a dependant type representing all the vectors
+A dependent type is a type which depends on some term. For instance
+``vector of size n'' is a dependent type representing all the vectors
 of size $n$. Its type depends on $n$
 
 \Question{What is a proof by reflection?}
diff --git a/lib/profile.ml b/lib/profile.ml
index 0910db3fe2..d620fe69c4 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -146,9 +146,9 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
    number of allocated bytes may exceed the maximum integer capacity
    (2^31 on 32-bits architectures);  therefore, allocation is measured
    by small steps, total allocations are computed by adding elementary
-   measures and carries are controled from step to step *)
+   measures and carries are controlled from step to step *)
 
-(* Unix measure of time is approximative and shoitt delays are often
+(* Unix measure of time is approximate and short delays are often
    unperceivable; therefore, total times are measured in one (big)
    step to avoid rounding errors and to get the best possible
    approximation.
@@ -358,7 +358,7 @@ let declare_profile name =
   prof_table := (name,e)::!prof_table;
   e
 
-(* Default initialisation, may be overriden *)
+(* Default initialization, may be overridden *)
 let _ = init_profile ()
 
 (******************************)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7605f63872..e753e972da 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -617,7 +617,7 @@ module Bullet = struct
     let _ = register_behavior strict
   end
 
-  (* Current bullet behavior, controled by the option *)
+  (* Current bullet behavior, controlled by the option *)
   let current_behavior = ref Strict.strict
 
   let _ =
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 13cb559b99..5acdb7eb7e 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.S] using lists of pairs ordered (increasing) with respect to
  left projection. *)
 
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0f11dd7a53..130cbee871 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
 Require Import FMapInterface.
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 1f36306c34..9c3ec71ae3 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.S] using strictly ordered list. *)
 
 Require Export FSetInterface.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 2ea32e97cb..9dbea88495 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.WS] using lists without redundancy. *)
 
 Require Import FSetInterface.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index fb0d1ad9df..05c20eb8fa 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [MSetInterface.S] using strictly ordered list. *)
 
 Require Export MSetInterface OrdersFacts OrdersLists.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 372acd56ad..2ac57a932b 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [MSetWeakInterface.S] using lists without redundancy. *)
 
 Require Import MSetInterface.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 230e62607a..41ee165ff8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1127,7 +1127,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   (* Parts of this code are overly complicated because the implicit arguments
      API is completely crazy: positions (ExplByPos) are elaborated to
      names. This is broken by design, since not all arguments have names. So
-     eventhough we eventually want to map only positions to implicit statuses,
+     even though we eventually want to map only positions to implicit statuses,
      we have to check whether the corresponding arguments have names, not to
      trigger an error in the impargs code. Even better, the names we have to
      check are not the current ones (after previous renamings), but the original
@@ -2135,7 +2135,7 @@ let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
   | Some b -> Flags.make_polymorphic_flag b; b
 
-(** A global default timeout, controled by option "Set Default Timeout n".
+(** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
 let default_timeout = ref None
-- 
cgit v1.2.3


From 3642314974b3aca6eb522c37e7e4efd226e6ebc8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 29 Nov 2016 17:50:11 +0100
Subject: STM: cur_id must be invalid if an error occurs (fix #5191)

Line erroneously removed in 17f3346c
---
 stm/stm.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index e387e6322f..b4331dc460 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -896,6 +896,7 @@ end = struct (* {{{ *)
     with e ->
       let (e, info) = CErrors.push e in
       let good_id = !cur_id in
+      cur_id := Stateid.dummy;
       VCS.reached id;
       let ie =
         match Stateid.get info, safe_id with
-- 
cgit v1.2.3


From 89fc7443d2e35f5020d272faecc4fe1f6e12eb11 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Nov 2016 11:37:24 +0100
Subject: Fix #5174: Underinformative syntax error messages in the new
 arguments syntax

We introduce a bit of compatibility parsing code to print deprecation
warnings.
---
 parsing/g_vernac.ml4 | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9b52d1bf31..e61be53a99 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -582,9 +582,9 @@ let warn_deprecated_implicit_arguments =
 
 let warn_deprecated_arguments_syntax =
   CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated"
-         (fun () -> strbrk "The \"/\" modifier has an effect only in the first "
-                    ++ strbrk "arguments list. The syntax allowing it to appear"
-                    ++ strbrk " in other lists is deprecated.")
+         (fun () -> strbrk "The \"/\" and \"!\" modifiers have an effect only "
+                    ++ strbrk "in the first arguments list. The syntax allowing"
+                    ++ strbrk " them to appear in other lists is deprecated.")
 
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
@@ -664,8 +664,8 @@ GEXTEND Gram
         more_implicits = OPT
           [ ","; impl = LIST1
             [ impl = LIST0 more_implicits_block ->
-              let warn_slash = List.exists fst impl in
-              if warn_slash then warn_deprecated_arguments_syntax ~loc:!@loc ();
+              let warn_deprecated = List.exists fst impl in
+              if warn_deprecated then warn_deprecated_arguments_syntax ~loc:!@loc ();
               List.flatten (List.map snd impl)]
             SEP "," -> impl
           ];
@@ -776,14 +776,19 @@ GEXTEND Gram
                  implicit_status = MaximallyImplicit}) items
     ]
   ];
+  name_or_bang: [
+       [ b = OPT "!"; id = name ->
+       not (Option.is_empty b), id
+    ]
+  ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
-    [ name = name -> (false, [(snd name, Vernacexpr.NotImplicit)])
+    [ (bang,name) = name_or_bang -> (bang, [(snd name, Vernacexpr.NotImplicit)])
     | "/" -> (true (* Should warn about deprecated syntax *), [])
-    | "["; items = LIST1 name; "]" ->
-       (false, List.map (fun name -> (snd name, Vernacexpr.Implicit)) items)
-    | "{"; items = LIST1 name; "}" ->
-       (false, List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items)
+    | "["; items = LIST1 name_or_bang; "]" ->
+       (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.Implicit)) items)
+    | "{"; items = LIST1 name_or_bang; "}" ->
+       (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.MaximallyImplicit)) items)
     ]
   ];
   strategy_level:
-- 
cgit v1.2.3


From b6a70501e7ba46d556288abc5c3c81399a280e26 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Nov 2016 16:29:24 +0100
Subject: Update copyright on documentation cover.

---
 doc/common/styles/html/coqremote/cover.html | 1 +
 doc/common/styles/html/simple/cover.html    | 1 +
 2 files changed, 2 insertions(+)

diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index 6ec4dc1af0..1c415eca69 100644
--- a/doc/common/styles/html/coqremote/cover.html
+++ b/doc/common/styles/html/coqremote/cover.html
@@ -61,6 +61,7 @@
   <li>V8.3 © INRIA 2010-2011</li>
   <li>V8.4 © INRIA 2012-2014</li>
   <li>V8.5 © INRIA 2015-2016</li>
+  <li>V8.6 © INRIA 2016</li>
 </ul>
 
 <p style="text-indent:0pt">This research was partly supported by IST
diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html
index 328bd68daf..25fb56320b 100644
--- a/doc/common/styles/html/simple/cover.html
+++ b/doc/common/styles/html/simple/cover.html
@@ -39,6 +39,7 @@
   <li>V8.3 © INRIA 2010-2011</li>
   <li>V8.4 © INRIA 2012-2014</li>
   <li>V8.5 © INRIA 2015-2016</li>
+  <li>V8.6 © INRIA 2016</li>
 </ul>
 
 <p style="text-indent:0pt">This research was partly supported by IST
-- 
cgit v1.2.3


From 3e6fa1cbdc0ec145728089000595b6ea29f37a4c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 29 Nov 2016 16:35:56 +0100
Subject: Fix #5183 - Two CoqIDE crash errors

When opening a file without extension, an uncaught exception was
occurring.

Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
---
 lib/aux_file.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c6c7b42429..0f0f09aa23 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -17,6 +17,10 @@ let version = 1
 
 let oc = ref None
 
+let chop_extension f =
+  if check_suffix f ".v" then chop_extension f
+  else f
+
 let aux_file_name_for vfile =
   dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
 
-- 
cgit v1.2.3