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 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