From ac9f2b1a5789964b1d881d024912350a7506a0f9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 4 Dec 2016 11:40:36 +0100
Subject: [pp] Set printing width for richpp formatter (bug #5244)

Richpp output depends on printing width, thus its internal formatter
should be seeded with the proper width value.

While we are at it, we increase the default buffer size to a more
sensible value.
---
 lib/richpp.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/lib/richpp.ml b/lib/richpp.ml
index a98273edb2..d1c6d158e4 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -55,7 +55,7 @@ let rich_pp annotate ppcmds =
     string_of_int index
   in
 
-  let pp_buffer = Buffer.create 13 in
+  let pp_buffer = Buffer.create 180 in
 
   let push_pcdata () =
     (** Push the optional PCData on the above node *)
@@ -113,6 +113,13 @@ let rich_pp annotate ppcmds =
   pp_set_formatter_tag_functions ft tag_functions;
   pp_set_mark_tags ft true;
 
+  (* Set formatter width. This is currently a hack and duplicate code
+     with Pp_control. Hopefully it will be fixed better in Coq 8.7 *)
+  let w = pp_get_margin str_formatter () in
+  let m = max (64 * w / 100) (w-30) in
+  pp_set_margin ft w;
+  pp_set_max_indent ft m;
+
   (** The whole output must be a valid document. To that
       end, we nest the document inside <pp> tags. *)
   pp_open_tag ft "pp";
-- 
cgit v1.2.3


From ac630f12c9d80c9387d44f3f1a1b22db5b5b89da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Dec 2016 13:48:01 +0100
Subject: Fixing anomaly EqUnknown in Equality Scheme (#5278).

---
 toplevel/auto_ind_decl.ml | 18 +++++++++---------
 toplevel/indschemes.ml    |  3 +++
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b3144fa927..a527be32ba 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -204,19 +204,19 @@ let build_beq_scheme mode kn =
             end
         | Sort _  -> raise InductiveWithSort
         | Prod _ -> raise InductiveWithProduct
-        | Lambda _-> raise (EqUnknown "Lambda")
-        | LetIn _ -> raise (EqUnknown "LetIn")
+        | Lambda _-> raise (EqUnknown "abstraction")
+        | LetIn _ -> raise (EqUnknown "let-in")
         | Const kn ->
 	    (match Environ.constant_opt_value_in env kn with
 	      | None -> raise (ParameterWithoutEquality (fst kn))
 	      | Some c -> aux (applist (c,a)))
-        | Proj _ -> raise (EqUnknown "Proj")
-        | Construct _ -> raise (EqUnknown "Construct")
-        | Case _ -> raise (EqUnknown "Case")
-        | CoFix _ -> raise (EqUnknown "CoFix")
-        | Fix _   -> raise (EqUnknown "Fix")
-        | Meta _  -> raise (EqUnknown "Meta")
-        | Evar _  -> raise (EqUnknown "Evar")
+        | Proj _ -> raise (EqUnknown "projection")
+        | Construct _ -> raise (EqUnknown "constructor")
+        | Case _ -> raise (EqUnknown "match")
+        | CoFix _ -> raise (EqUnknown "cofix")
+        | Fix _   -> raise (EqUnknown "fix")
+        | Meta _  -> raise (EqUnknown "meta-variable")
+        | Evar _  -> raise (EqUnknown "existential variable")
     in
       aux t
   in
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index aa2362ae5f..0e59f1aa98 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -185,6 +185,9 @@ let try_declare_scheme what f internal names kn =
     | DecidabilityMutualNotSupported ->
         alarm what internal
           (str "Decidability lemma for mutual inductive types not supported.")
+    | EqUnknown s ->
+         alarm what internal
+           (str "Found unsupported " ++ str s ++ str " while building Boolean equality.")
     | e when Errors.noncritical e ->
         alarm what internal
 	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
-- 
cgit v1.2.3


From 3b821bf60d89c386c27487e172e57a669b5c4662 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 23 Dec 2016 11:53:17 +0100
Subject: Excluding explicitly coinductive types in Scheme Equality (#5284).

---
 toplevel/auto_ind_decl.ml  | 3 +++
 toplevel/auto_ind_decl.mli | 1 +
 toplevel/indschemes.ml     | 3 +++
 3 files changed, 7 insertions(+)

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index a527be32ba..ace99b7bbe 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -56,6 +56,7 @@ exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
+exception NoDecidabilityCoInductive
 
 let dl = Loc.ghost
 
@@ -301,6 +302,8 @@ let build_beq_scheme mode kn =
       let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
 	if not (Sorts.List.mem InSet kelim) then
 	  raise (NonSingletonProp (kn,i));
+        if mib.mind_finite = Decl_kinds.CoFinite then
+	  raise NoDecidabilityCoInductive;
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
         create_input fix),
        Evd.make_evar_universe_context (Global.env ()) None),
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index b6c66a1e84..bdfe6e3fa7 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -24,6 +24,7 @@ exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
+exception NoDecidabilityCoInductive
 
 val beq_scheme_kind : mutual scheme_kind
 val build_beq_scheme : mutual_scheme_object_function
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 0e59f1aa98..a430d0ded2 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -188,6 +188,9 @@ let try_declare_scheme what f internal names kn =
     | EqUnknown s ->
          alarm what internal
            (str "Found unsupported " ++ str s ++ str " while building Boolean equality.")
+    | NoDecidabilityCoInductive ->
+         alarm what internal
+           (str "Scheme Equality is only for inductive types.")
     | e when Errors.noncritical e ->
         alarm what internal
 	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
-- 
cgit v1.2.3


From 827370fb97c138c16509bd549eaeddf94ca13c99 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 617185b8fe..5e4e6645a4 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -823,7 +823,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 dd710b9adbe7b27dccd6d4b21b90cb9bd07e5c07 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 26 Dec 2016 10:02:34 +0100
Subject: Fix some documentation typos.

---
 CHANGES                          | 4 ++--
 config/coq_config.mli            | 4 ++--
 dev/doc/notes-on-conversion      | 2 +-
 doc/faq/FAQ.tex                  | 4 ++--
 ide/utils/configwin_keys.ml      | 2 +-
 lib/profile.ml                   | 6 +++---
 parsing/pcoq.mli                 | 4 ++--
 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 +-
 theories/Numbers/BigNumPrelude.v | 4 ++--
 theories/Strings/Ascii.v         | 2 +-
 toplevel/vernacentries.ml        | 2 +-
 17 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/CHANGES b/CHANGES
index 97106aaf15..6b620e4a48 100644
--- a/CHANGES
+++ b/CHANGES
@@ -991,7 +991,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"
@@ -1676,7 +1676,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 f250059316..269b68e4f6 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -37,7 +37,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 *)
 
 
@@ -56,7 +56,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/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/lib/profile.ml b/lib/profile.ml
index 2350cd43ac..13c2d9c802 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/parsing/pcoq.mli b/parsing/pcoq.mli
index 54e6423877..a44d942992 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -40,7 +40,7 @@ module Gram : GrammarSig
         |     (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
         |
@@ -128,7 +128,7 @@ val type_of_typed_entry : typed_entry -> entry_type
 val object_of_typed_entry : typed_entry -> grammar_object Gram.entry
 val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry
 
-(** Temporary activate camlp4 verbosity *)
+(** Temporarily activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 541f299d4f..b00ecfad8a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -610,7 +610,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/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 :=
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c76432ae3e..1328019713 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2050,7 +2050,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 aad7ca30a093190be17ac504b8a36cb04ae928de Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 6 Dec 2016 17:52:26 +0100
Subject: Update documentation (bugs #5246 and #5251).

---
 doc/refman/RefMan-gal.tex | 6 +++---
 doc/refman/RefMan-tac.tex | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index fcccd9cb4b..5880b6c848 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -711,9 +711,9 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
            {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
  & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
            & & \\
-{\inductivebody} & ::= & 
-  {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\
-   && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\
+{\inductivebody} & ::= &
+  {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\
+   && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\
            & & \\  %% TODO: where ...
 %% Fixpoints
 {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 11de4f35e0..d539af7e31 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -292,7 +292,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
 {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}.
 
 \begin{ErrMsgs}
-\item \errindex{Impossible to unify \dots\ with \dots}
+\item \errindex{Unable to unify \dots\ with \dots}
 
   The {\tt apply}
   tactic failed to match the conclusion of {\term} and the current goal.
@@ -4593,7 +4593,7 @@ It is equivalent to {\tt apply refl\_equal}.
 
 \begin{ErrMsgs}
 \item \errindex{The conclusion is not a substitutive equation}
-\item \errindex{Impossible to unify \dots\ with \dots}
+\item \errindex{Unable to unify \dots\ with \dots}
 \end{ErrMsgs}
 
 \subsection{\tt symmetry}
-- 
cgit v1.2.3


From 5f358c91347d4bbc2f4543012ff8b4bf3dab71c9 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 6 Dec 2016 18:53:22 +0100
Subject: Fix broken documentation in presence of \zeroone{... \tt ...}.

The way \zeroone was defined, the \tt modifier was leaked outside the
brackets, thus messing with the following text. There are a bunch of
occurrences of this issue in the manual, so rather than turning all the
\tt into \texttt, the definition of \zeroone is made more robust.

Unfortunately, there is one single occurrence of \zeroone that does not
support the more robust version. (Note that this specific usage of
\zeroone is morally a bug, since it goes against all the LaTeX
conventions.) So the commit also keeps the old leaky version of \zeroone
around as \zeroonelax so that it can be used there.
---
 doc/common/macros.tex     | 3 ++-
 doc/refman/RefMan-tac.tex | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index bbc78a8517..ce89c5b93e 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -72,7 +72,8 @@
 %\newcommand{\spec}[1]{\{\,#1\,\}}
 
 % Building regular expressions
-\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
+\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}}
+\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
 %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
 %\newcommand{\onemany}[1]{$\{$#1$\}$+}
 \newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d539af7e31..d05f74f72a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -114,7 +114,7 @@ following syntax:
 \begin{tabular}{lcl}
 {\occclause} & ::= & {\tt in} {\occgoalset} \\
 {\occgoalset} & ::= &
-    \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
+    \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
 &   & {\dots} {\tt ,}\\
 &   & {\ident$_m$} \zeroone{\atoccurrences}}\\
 &   & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\
-- 
cgit v1.2.3


From 63ca4aac83ced14b9b8065ef43e29f7c2dfd331c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 23 Dec 2016 09:28:47 +0100
Subject: Handle application of a primitive projection to a not yet evaluated
 cofixpoint (bug #5286).

---
 kernel/byterun/coq_interp.c | 63 ++++++++++++++++++++++++++++++++++-----------
 1 file changed, 48 insertions(+), 15 deletions(-)

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 35abd011bb..a67c27e87f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -898,25 +898,58 @@ value coq_interprete
 
 
       Instruct(PROJ){
+        do_proj:
 	print_instr("PROJ");
 	if (Is_accu (accu)) {
-          value block;
-	  /* Skip over the index of projected field */
-	  pc++;
-	  /* Create atom */
-	  Alloc_small(block, 2, ATOM_PROJ_TAG);
-	  Field(block, 0) = Field(coq_global_data, *pc);
-	  Field(block, 1) = accu;
-          accu = block;
-          /* Create accumulator */
-          Alloc_small(block, 2, Accu_tag);
-          Code_val(block) = accumulate;
-          Field(block, 1) = accu;
-          accu = block;
+          *--sp = accu; // Save matched block on stack
+          accu = Field(accu, 1); // Save atom to accu register
+          switch (Tag_val(accu)) {
+          case ATOM_COFIX_TAG: // We are forcing a cofix
+            {
+              mlsize_t i, nargs;
+              sp -= 2;
+              // Push the current instruction as the return address
+              sp[0] = (value)(pc - 1);
+              sp[1] = coq_env;
+              coq_env = Field(accu, 0); // Pointer to suspension
+              accu = sp[2]; // Save accumulator to accu register
+              sp[2] = Val_long(coq_extra_args); // Push number of args for return
+              nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+              // Push arguments to stack
+              CHECK_STACK(nargs + 1);
+              sp -= nargs;
+              for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2);
+              *--sp = accu; // Last argument is the pointer to the suspension
+              coq_extra_args = nargs;
+              pc = Code_val(coq_env); // Trigger evaluation
+              goto check_stack;
+            }
+          case ATOM_COFIXEVALUATED_TAG:
+            {
+              accu = Field(accu, 1);
+              ++sp;
+              goto do_proj;
+            }
+          default:
+            {
+              value block;
+              /* Skip over the index of projected field */
+              ++pc;
+              /* Create atom */
+              Alloc_small(accu, 2, ATOM_PROJ_TAG);
+              Field(accu, 0) = Field(coq_global_data, *pc++);
+              Field(accu, 1) = *sp++;
+              /* Create accumulator */
+              Alloc_small(block, 2, Accu_tag);
+              Code_val(block) = accumulate;
+              Field(block, 1) = accu;
+              accu = block;
+            }
+          }
 	} else {
-	    accu = Field(accu, *pc++);
+          accu = Field(accu, *pc);
+          pc += 2;
 	}
-	pc++;
 	Next;
       }
 
-- 
cgit v1.2.3


From 65816f94ba427edf8999bf42633d0aad064e8ce4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Jan 2017 19:54:41 +0100
Subject: Fixing a little bug in printing cofix with no arguments.

---
 printing/ppconstr.ml           | 2 +-
 test-suite/output/Fixpoint.out | 2 ++
 test-suite/output/Fixpoint.v   | 5 ++++-
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e21bfa007d..31d87f0ff1 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -418,7 +418,7 @@ end) = struct
   let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
     let pr_body =
       if dangling_with_for then pr_dangling else pr in
-    pr_id id ++ str" " ++
+    pr_id id ++ (if bl = [] then mt () else str" ") ++
       hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
       pr_opt_type_spc pr t ++ str " :=" ++
       pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index a13ae4624a..6879cbc3c2 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -10,3 +10,5 @@ let fix f (m : nat) : nat := match m with
                              end in f 0
      : nat
 Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
+     = cofix inf : Inf := {| projS := inf |}
+     : Inf
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 8afa50ba57..fafb478bad 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,4 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   omega.
 Qed.
 
-
+CoInductive Inf := S { projS : Inf }.
+Definition expand_Inf (x : Inf) := S (projS x).
+CoFixpoint inf := S inf.
+Eval compute in inf.
-- 
cgit v1.2.3


From a9b76df171ceea443885bb4be919ea586a82beee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 20 Jan 2017 10:55:17 +0100
Subject: Do not add redundant side effects in tactic code.

This was observable in long proofs, because side effects kept being
duplicated, leading to an additional cost linear in the size of the proof.
This commit touches kernel files, but the corresponding API is only used
in tactic-facing code so that the side_effects type remains opaque. Thus
it does not affect the kernel safety.
---
 kernel/safe_typing.ml  | 4 ++--
 kernel/term_typing.mli | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 09f7bd75cd..95d9c75d30 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -213,8 +213,8 @@ type private_constant_role = Term_typing.side_effect_role =
   | Schema of inductive * string
 
 let empty_private_constants = []
-let add_private x xs = x :: xs
-let concat_private xs ys = xs @ ys
+let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs
+let concat_private xs ys = List.fold_right add_private xs ys
 let mk_pure_proof = Term_typing.mk_pure_proof
 let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index fcd95576c0..89b5fc40e3 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,6 +30,7 @@ val inline_entry_side_effects :
     yet type checked proof. *)
 
 val uniq_seff : side_effects -> side_effects
+val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
   structure_body -> env -> constant -> side_effects constant_entry ->
-- 
cgit v1.2.3


From 1d4c34c79624fb81e64dfed8874b2fc9fa66c070 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Jan 2017 13:51:37 +0100
Subject: Process Next Obligation proofs in parallel (fix #5314)

---
 intf/vernacexpr.mli    | 3 +++
 ltac/g_obligations.ml4 | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 92e4dd618e..c9fb1b5986 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -524,6 +524,9 @@ and vernac_control =
   | VtObserve of Stateid.t
   | VtBack of Stateid.t
   | VtPG
+(* Qed typically generates an opaque proof term.  Still, by declaring
+ * a proof terminator one can use such opaque term to generate transparent
+ * ones.  In this corner case the STM needs to know... *)
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index 987b9d5387..2ae183e6e9 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -66,7 +66,7 @@ GEXTEND Gram
 
 open Obligations
 
-let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater)
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
 | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
-- 
cgit v1.2.3


From 6ff62ec78d5517ec5905041fa2e4926e15ff89f0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 21 Jan 2017 07:51:15 +0100
Subject: Revert "Process Next Obligation proofs in parallel (fix #5314)"

This reverts commit 1d4c34c79624fb81e64dfed8874b2fc9fa66c070.

It seems the proof terminator of obligation.ml, in the case in which
Set Shrink Obligation is set, accesses the opaque proof.
---
 intf/vernacexpr.mli    | 3 ---
 ltac/g_obligations.ml4 | 2 +-
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index c9fb1b5986..92e4dd618e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -524,9 +524,6 @@ and vernac_control =
   | VtObserve of Stateid.t
   | VtBack of Stateid.t
   | VtPG
-(* Qed typically generates an opaque proof term.  Still, by declaring
- * a proof terminator one can use such opaque term to generate transparent
- * ones.  In this corner case the STM needs to know... *)
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index 2ae183e6e9..987b9d5387 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -66,7 +66,7 @@ GEXTEND Gram
 
 open Obligations
 
-let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater)
+let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
 | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
-- 
cgit v1.2.3


From e91ae93106b6bd6d92ef53ac18b04654485a8106 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Jan 2017 10:52:18 +0100
Subject: Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs
 with let-ins).

A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.

This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.

Thanks to Jason for helping in diagnosing the problem.
---
 pretyping/cases.ml            | 10 ++++++----
 test-suite/bugs/closed/5322.v | 14 ++++++++++++++
 test-suite/success/Case22.v   | 28 ++++++++++++++++++++++++++++
 3 files changed, 48 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/5322.v

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6e4d72705b..ef3e53bf1f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -847,7 +847,7 @@ let subst_predicate (subst,copt) ccl tms =
     | Some c -> c::subst in
   substnl_predicate sigma 0 ccl tms
 
-let specialize_predicate_var (cur,typ,dep) tms ccl =
+let specialize_predicate_var (cur,typ,dep) env tms ccl =
   let c = match dep with
   | Anonymous -> None
   | Name _ -> Some cur
@@ -855,7 +855,9 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
   let l =
     match typ with
     | IsInd (_, IndType (_, _), []) -> []
-    | IsInd (_, IndType (_, realargs), names) -> realargs
+    | IsInd (_, IndType (indf, realargs), names) ->
+       let arsign,_ = get_arity env indf in
+       subst_of_rel_context_instance arsign realargs
     | NotInd _ -> [] in
   subst_predicate (l,c) ccl tms
 
@@ -1390,7 +1392,7 @@ and match_current pb (initial,tomatch) =
 and shift_problem ((current,t),_,na) pb =
   let ty = type_of_tomatch t in
   let tomatch = lift_tomatch_stack 1 pb.tomatch in
-  let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
   let pb =
     { pb with
        env = push_rel (LocalDef (na,current,ty)) pb.env;
@@ -1407,7 +1409,7 @@ and shift_problem ((current,t),_,na) pb =
    are already introduced in the context, we avoid creating aliases to
    themselves by treating this case specially. *)
 and pop_problem ((current,t),_,na) pb =
-  let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
   let pb =
     { pb with
        pred = pred;
diff --git a/test-suite/bugs/closed/5322.v b/test-suite/bugs/closed/5322.v
new file mode 100644
index 0000000000..01aec8f29b
--- /dev/null
+++ b/test-suite/bugs/closed/5322.v
@@ -0,0 +1,14 @@
+(* Regression in computing types of branches in "match" *)
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := a : op Unit Unit.
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2.
+  refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with
+         | _ => _
+         end.
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 3c696502cd..465b3eb8c0 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -41,6 +41,7 @@ Definition F (x:IND True) (A:Type) :=
 Theorem paradox : False.
   (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
 Fail Proof (F C False).
+Abort.
 
 (* Another bug found in November 2015 (a substitution was wrongly
    reversed at pretyping level) *)
@@ -61,3 +62,30 @@ Inductive Ind2 (b:=1) (c:nat) : Type :=
   Constr2 : Ind2 c.
 
 Eval vm_compute in Constr2 2.
+
+(* A bug introduced in ade2363 (similar to #5322 and #5324). This
+   commit started to see that some List.rev was wrong in the "var"
+   case of a pattern-matching problem but it failed to see that a
+   transformation from a list of arguments into a substitution was
+   still needed. *)
+
+(* The order of real arguments was made wrong by ade2363 in the "var"
+   case of the compilation of "match" *)
+
+Inductive IND2 : forall X Y:Type, Type :=
+  CONSTR2 : IND2 unit Empty_set.
+
+Check fun x:IND2 bool nat =>
+  match x in IND2 a b return a with
+  | y => _
+  end = true.
+
+(* From January 2017, using the proper function to turn arguments into
+   a substitution up to a context possibly containing let-ins, so that
+   the following, which was wrong also before ade2363, now works
+   correctly *)
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | y => (true,0)
+  end.
-- 
cgit v1.2.3


From a6f687852c0c7509a06fdf16c0af29129b3566d5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Jan 2017 10:32:08 +0100
Subject: Fixing unification regression #5323.

Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed).
---
 pretyping/evd.ml              |  5 ++++-
 test-suite/bugs/closed/5323.v | 26 ++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/5323.v

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2f4b8fc12f..7b0ffd8b1d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -898,13 +898,16 @@ let restrict evk evk' filter ?candidates evd =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }
+    defn_evars; last_mods; evar_names }
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
diff --git a/test-suite/bugs/closed/5323.v b/test-suite/bugs/closed/5323.v
new file mode 100644
index 0000000000..295b7cd9f5
--- /dev/null
+++ b/test-suite/bugs/closed/5323.v
@@ -0,0 +1,26 @@
+(* Revealed a missing re-consideration of postponed problems *)
+
+Module A.
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type 
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := .
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2
+  := match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with end.
+End A.
+
+(* A shorter variant *)
+Module B.
+Inductive exprf (op : unit -> Type) : Type :=
+| A : exprf op
+| Op tR (opc : op tR) (args : exprf op) : exprf op.
+Inductive op : unit -> Type := .
+Definition bound_op (dst2 : unit) (opc2 : op dst2)
+  : forall (args2 : exprf op), Op op dst2 opc2 args2 = A op
+  := match opc2 in op h return (forall args2 : exprf ?[U], Op ?[V] ?[I] opc2 args2 = A op) with end.
+End B.
-- 
cgit v1.2.3


From 180775636f5ec93e95df681951fafb321f8ebe67 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 26 Jan 2017 00:53:23 +0100
Subject: Fixing #5326 (anomaly on some unsupported case of 'pat).

We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
---
 interp/topconstr.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 79eeacf354..d388376bc2 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -92,8 +92,9 @@ let rec fold_local_binders g f n acc b = function
       f n (fold_local_binders g f n' acc b l) t
   | LocalRawDef ((_,na),t)::l ->
       f n (fold_local_binders g f (name_fold g na n) acc b l) t
-  | LocalPattern _::l ->
-      assert false
+  | LocalPattern (_,pat,t)::l ->
+      let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
+      Option.fold_left (f n) acc t
   | [] ->
       f n acc b
 
-- 
cgit v1.2.3


From 86116b181bb866c7f63a37796e1388f731ce7204 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Jan 2017 11:38:19 +0100
Subject: [native comp] Improve error message on linking error.

The native compiler doesn't support `Require` inside `Module` sections
in some cases, we improve the error message. See:

https://coq.inria.fr/bugs/show_bug.cgi?id=4335

This patch improves the error message and gives the user some
feedback.
---
 kernel/safe_typing.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b28cd87bd..7e28b1c567 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -795,7 +795,10 @@ type compiled_library = {
 type native_library = Nativecode.global list
 
 let get_library_native_symbols senv dir =
-  DPMap.find dir senv.native_symbols
+  try DPMap.find dir senv.native_symbols
+  with Not_found -> Errors.errorlabstrm "get_library_native_symbols"
+                      Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++
+                          (str "This use case is not supported, but disabling the native compiler may help."))
 
 (** FIXME: MS: remove?*)
 let current_modpath senv = senv.modpath
-- 
cgit v1.2.3


From 22e2e5722d233bbd939cd235650497e30e506e63 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 27 Jan 2017 09:29:53 +0100
Subject: Fix documentation typos.

---
 ide/interface.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ide/interface.mli b/ide/interface.mli
index 2a9b8b241f..123cac6c22 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -139,7 +139,7 @@ type add_rty = state_id * ((unit, state_id) union * string)
     [Inr (start,(stop,tip))] if [id] is in a zone that can be focused.
     In that case the zone is delimited by [start] and [stop] while [tip]
     is the new document [tip].  Edits made by subsequent [add] are always
-    performend on top of [id]. *)
+    performed on top of [id]. *)
 type edit_at_sty = state_id
 type edit_at_rty = (unit, state_id * (state_id * state_id)) union
 
@@ -153,7 +153,7 @@ type query_rty = string
 type goals_sty = unit
 type goals_rty = goals option
 
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
+(** Retrieve the list of uninstantiated evars in the current proof. [None] if no
     proof is in progress. *)
 type evars_sty = unit
 type evars_rty = evar list option
-- 
cgit v1.2.3


From 6e4c4578044c15ec172009a570d13b9e168cb93e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Jan 2017 19:02:20 +0100
Subject: Fix bug #5262: Error should tell me which name is duplicated.

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

diff --git a/toplevel/record.ml b/toplevel/record.ml
index ef09f6fa54..b8dcf81fde 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -550,8 +550,10 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
     | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
     | _ -> acc in
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (List.distinct_f Id.compare allnames)
-  then error "Two objects have the same name";
+  let () = match List.duplicates Id.equal allnames with
+  | [] -> ()
+  | id :: _ -> errorlabstrm "" (str "Two objects have the same name" ++ spc () ++ quote (Id.print id))
+  in
   let isnot_class = match kind with Class false -> false | _ -> true in
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";
-- 
cgit v1.2.3


From a54dccb53fa8d6c12745b5f7b2c3c993a915b5bd Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Dec 2016 12:23:14 +0100
Subject: Fix a typo in STM universe communications.

---
 stm/asyncTaskQueue.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index fa6422cdc5..8acc3c233a 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -170,7 +170,7 @@ module Make(T : Task) = struct
         | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
         | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
     let more_univs n =
-      CList.init 10 (fun _ ->
+      CList.init n (fun _ ->
         Universes.new_univ_level (Global.current_dirpath ())) in
 
     let rec kill_if () =
-- 
cgit v1.2.3


From f5923c2174fbb419397f127af31ab1cd0b223e0a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Jan 2017 06:36:25 +0100
Subject: Fixing #5311 (anomaly on unexpected intro pattern).

This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
---
 tactics/tacinterp.ml          |  2 +-
 test-suite/bugs/closed/5331.v | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/5331.v

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 23d188aa73..2cfd2d6b12 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -894,7 +894,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function
       (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
       | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
       | _ ->
-        raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
+        user_err_loc (loc,"", str "Cannot coerce to a disjunctive/conjunctive pattern."))
   | Some (ArgArg (loc,l)) ->
       let sigma,l = interp_or_and_intro_pattern ist env sigma l in
       sigma, Some (loc,l)
diff --git a/test-suite/bugs/closed/5331.v b/test-suite/bugs/closed/5331.v
new file mode 100644
index 0000000000..0d72fcb5df
--- /dev/null
+++ b/test-suite/bugs/closed/5331.v
@@ -0,0 +1,11 @@
+(* Checking no anomaly on some unexpected intropattern *)
+
+Ltac ih H := induction H as H.
+Ltac ih' H H' := induction H as H'.
+
+Goal True -> True.
+Fail intro H; ih H.
+intro H; ih' H ipattern:[].
+exact I.
+Qed.
+
-- 
cgit v1.2.3