Merge branch 'v8.6'

27 files changed, 51 insertions, 42 deletions

diff --git a/CHANGES b/CHANGES
index 7ee0c7373..090f7c13b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1139,7 +1139,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"
@@ -1824,7 +1824,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 6087c0116..c171bd355 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 6274275c9..a81f170c6 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/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index 6ec4dc1af..1c415eca6 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 328bd68da..25fb56320 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
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 48b61827d..213fb0313 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/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 792a311fc..47df22807 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;
       }
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c6c7b4242..0f0f09aa2 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"
 
diff --git a/lib/profile.ml b/lib/profile.ml
index 0910db3fe..d620fe69c 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/ltac/pptactic.ml b/ltac/pptactic.ml
index 6230fa060..85740f187 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -1083,7 +1083,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
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b3233f8f0..d46880831 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -767,6 +767,11 @@ 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 -> [(snd name, Vernacexpr.NotImplicit)]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 77884fb1c..d987bb455 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -38,7 +38,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
         |
@@ -95,7 +95,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
 
@@ -208,14 +208,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/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a063cbbfe..e4b58a56f 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))
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2956d623f..a2ee62221 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -622,7 +622,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/stm/stm.ml b/stm/stm.ml
index 23d68c4b8..f7569d257 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
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 13cb559b9..5acdb7eb7 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 0f11dd7a5..130cbee87 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 1f36306c3..9c3ec71ae 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 2ea32e97c..9dbea8849 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 fb0d1ad9d..05c20eb8f 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 372acd56a..2ac57a932 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/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 45a7527c9..bd8930872 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 97cb746f3..55a533c55 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 :=
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ac69a69a4..eab909f5b 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;
diff --git a/tools/coqc.ml b/tools/coqc.ml
index b59bbdb1e..b12d48710 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 956a40261..38ceacf5e 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\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cd61bf7ff..8ce13c69a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1128,7 +1128,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
@@ -2136,7 +2136,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