From 5f49780b395686cdfce7126438c6dd69712d5c70 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 13 Jan 2015 19:54:26 +0100
Subject: Bump version and magic numbers in configure.

---
 configure.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/configure.ml b/configure.ml
index 4e2e34641a..d68fc505d0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,11 +11,11 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "trunk"
-let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of
+let coq_version = "8.5beta1"
+let coq_macos_version = "8.5.91" (** "[...] should be a string comprised of
 three non-negative, period-separed integers [...]" *)
-let vo_magic = 8511
-let state_magic = 58511
+let vo_magic = 8591
+let state_magic = 58501
 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert"]
 
-- 
cgit v1.2.3


From 6303fce370131b7e0c648b4fd85565f9ec2203db Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 11:27:17 +0100
Subject: CHANGES: my recent updates to Ltac.

- gfail
- multimatch
- tryif/then/else---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGES b/CHANGES
index b5b379eca8..4a9c3a40d8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -118,6 +118,9 @@ Tactics
     the need of the undocumented "constructor <tac>" syntax which is
     now equivalent to "once (constructor; tac)". (potential source of
     rare incompatibilities).
+  * New "multimatch" variant of "match" tactic which backtracks to
+    new branches in case of a later failure. The "match" tactic is
+    equivalent to "once multimatch".
   * New selector all: to qualify a tactic allows applying a tactic to
     all the focused goal, instead of just the first one as is the
     default.
@@ -140,6 +143,8 @@ Tactics
     Accompanied by "guard" tactic which fails if a Boolean test does
     not pass.
   * New tactical "[> ... ]" to apply tactics to individual goals.
+  * New tactic "gfail" which works like "fail" except it will also
+    fail if every goal has been solved.
   * The refine tactic is changed not to use an ad hoc typing algorithm
     to generate subgoals. It also uses the dependent subgoal feature
     to generate goals to materialize every existential variable which
@@ -156,6 +161,8 @@ Tactics
 - Matching using "lazymatch" was fundamentally modified. It now behaves
   like "match" (immediate execution of the matching branch) but without
   the backtracking mechanism in case of failure.
+- New "tryif t then u else v" tactical which executes "u" in case of success
+  of "t" and "v" in case of failure.
 - New conversion tactic "native_compute": evaluates the goal (or an hypothesis)
   with a call-by-value strategy, using the OCaml native compiler. Useful on
   very intensive computations.
-- 
cgit v1.2.3


From 61ca1ce53bf160a23fc4c8af4059d9efd742f1fb Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 11:41:16 +0100
Subject: Reference manual: document gfail.

---
 doc/refman/RefMan-ltac.tex | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 6f26c5eebf..dbb71a4142 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -133,6 +133,7 @@ is understood as
 & | & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
 & | & {\tt idtac} \sequence{\messagetoken}{}\\
 & | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
+& | & {\tt gfail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
 & | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\
 & | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\
 & | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
@@ -516,12 +517,14 @@ literally. If a (term) variable is given, its contents are printed.
 
 
 \subsubsection[Failing]{Failing\tacindex{fail}
-\index{Tacticals!fail@{\tt fail}}}
+\index{Tacticals!fail@{\tt fail}}
+\tacindex{gfail}\index{Tacticals!gfail@{\tt gfail}}}
 
 The tactic {\tt fail} is the always-failing tactic: it does not solve
 any goal. It is useful for defining other tacticals since it can be
 caught by {\tt try}, {\tt repeat}, {\tt match goal}, or the branching
-tacticals.
+tacticals. The {\tt fail} tactic will, however, succeed if all the
+goals have already been solved.
 
 \begin{Variants}
 \item {\tt fail $n$}\\ The number $n$ is the failure level. If no
@@ -539,6 +542,18 @@ The given tokens are used for printing the failure message.
 
 \item {\tt fail $n$ \nelist{\messagetoken}{}}\\
 This is a combination of the previous variants.
+
+\item {\tt gfail}\\
+This variant fails even if there are no goals left.
+
+\item {\tt gfail \nelist{\messagetoken}{}}\\
+{\tt gfail $n$ \nelist{\messagetoken}{}}\\
+These variants fail with an error message or an error level even if
+there are no goals left. Be careful however if Coq terms have to be
+printed as part of the failure: term construction always forces the
+tactic into the goals, meaning that if there are no goals when it is
+evaluated, a tactic call like {\tt let x:=H in fail 0 x} will succeed.
+
 \end{Variants}
 
 \ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}.
-- 
cgit v1.2.3


From 1fab386bc1a96951da011de2a5490c6dbe1b7248 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 12:00:24 +0100
Subject: Reference manual: try and improve the documentation of lazymatch.

In particular try to avoid the use of the word "backtracking" which refers to too many things.
---
 doc/refman/RefMan-ltac.tex | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index dbb71a4142..95467acd7f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -701,8 +701,12 @@ then a no-matching-clause error is raised.
 
 \item \index{lazymatch!in Ltac}
 \index{Ltac!lazymatch}
-Using {\tt lazymatch} instead of {\tt match} disables the backtracking
-mechanism.
+Using {\tt lazymatch} instead of {\tt match} will perform the same
+pattern matching procedure but will commit to the first matching
+branch rather than trying a new matching if the right-hand side
+fails. If the right-hand side of the selected branch is a tactic with
+backtracking points, then subsequent failures cause this tactic to
+backtrack.
 
 \item \index{context!in pattern}
 There is a special form of patterns to match a subterm against the
@@ -808,8 +812,12 @@ the {\tt match reverse goal with} variant.
 \index{Ltac!lazymatch goal}
 \index{lazymatch reverse goal!in Ltac}
 \index{Ltac!lazymatch reverse goal}
-Using {\tt lazymatch} instead of {\tt match} disables the backtracking
-mechanism.
+Using {\tt lazymatch} instead of {\tt match} will perform the same
+pattern matching procedure but will commit to the first matching
+branch with the first matching combination of hypotheses rather than
+trying a new matching if the right-hand side fails. If the right-hand
+side of the selected branch is a tactic with backtracking points, then
+subsequent failures cause this tactic to backtrack.
 
 \subsubsection[Filling a term context]{Filling a term context\index{context!in expression}}
 
-- 
cgit v1.2.3


From b63549edce71492617db99a75410256f1b0239b0 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 12:10:01 +0100
Subject: Reference manual: try and improve documentation for Ltac's match.

In particular document the "once" behaviour.
---
 doc/refman/RefMan-ltac.tex | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 95467acd7f..494905f225 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -685,6 +685,10 @@ pattern {\_} matches any term and shunts all remaining patterns if
 any. If all clauses fail (in particular, there is no pattern {\_})
 then a no-matching-clause error is raised.
 
+Failures in subsequent tactics do not cause backtracking to select new
+branches or inside the right-hand side of the selected branch even if
+it has backtracking points.
+
 \begin{ErrMsgs}
 
 \item \errindex{No matching clauses for match}
@@ -789,8 +793,12 @@ no other combination of hypotheses then the second proof context
 pattern is tried and so on. If the next to last proof context pattern
 fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$
 is applied. Note also that matching against subterms (using the {\tt
-context} {\ident} {\tt [} {\cpattern} {\tt ]}) is available and may
-itself induce extra backtrackings.
+context} {\ident} {\tt [} {\cpattern} {\tt ]}) is available and is
+also subject to yielding several matchings.
+
+Failures in subsequent tactics do not cause backtracking to select new
+branches or combinations of hypotheses, or inside the right-hand side
+of the selected branch even if it has backtracking points.
 
 \ErrMsg \errindex{No matching clauses for match goal}
 
-- 
cgit v1.2.3


From 5ec324ab5101be45c9cf9ffda9cbbbffde9b7df9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 14:04:02 +0100
Subject: Reference manual: document multimatch.

---
 doc/refman/RefMan-ltac.tex | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 494905f225..03facbdbb2 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -127,6 +127,12 @@ is understood as
 {\tt lazymatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
 & | &
 {\tt lazymatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
+& | &
+{\tt multimatch goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
+& | &
+{\tt multimatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
+& | &
+{\tt multimatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
 & | & {\tt abstract} {\atom}\\
 & | & {\tt abstract} {\atom} {\tt using} {\ident} \\
 & | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
@@ -703,6 +709,17 @@ it has backtracking points.
 
 \begin{Variants}
 
+\item \index{multimatch!in Ltac}
+\index{Ltac!multimatch}
+Using {\tt multimatch} instead of {\tt match} will allow subsequent
+tactics to backtrack into a right-hand side tactic which has
+backtracking points left and trigger the selection of a new matching
+branch when all the backtracking points of the right-hand side have
+been consumed.
+
+The syntax {\tt match \ldots} is, in fact, a shorthand for
+{\tt once multimatch \ldots}.
+
 \item \index{lazymatch!in Ltac}
 \index{Ltac!lazymatch}
 Using {\tt lazymatch} instead of {\tt match} will perform the same
@@ -816,6 +833,21 @@ first), but it possible to reverse this order (older first) with
 the {\tt match reverse goal with} variant.
 
 \variant
+
+\index{multimatch goal!in Ltac}
+\index{Ltac!multimatch goal}
+\index{multimatch reverse goal!in Ltac}
+\index{Ltac!multimatch reverse goal}
+
+Using {\tt multimatch} instead of {\tt match} will allow subsequent
+tactics to backtrack into a right-hand side tactic which has
+backtracking points left and trigger the selection of a new matching
+branch or combination of hypotheses when all the backtracking points
+of the right-hand side have been consumed.
+
+The syntax {\tt match [reverse] goal \ldots} is, in fact, a shorthand for
+{\tt once multimatch [reverse] goal \ldots}.
+
 \index{lazymatch goal!in Ltac}
 \index{Ltac!lazymatch goal}
 \index{lazymatch reverse goal!in Ltac}
-- 
cgit v1.2.3


From 9e809796dda907f39c4792a247d3156433de4fc4 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 14:44:03 +0100
Subject: Reference manual: document tryif/then/else.

---
 doc/refman/RefMan-ltac.tex | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 03facbdbb2..73bcc85871 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -108,6 +108,7 @@ is understood as
 {\tacexprinf} & ::= &
            {\tacexprlow} {\tt ||} {\tacexprpref}\\
 & | &      {\tacexprlow} {\tt +} {\tacexprpref}\\
+& | &      {\tt tryif} {\tacexprlow} {\tt then} {\tacexprlow} {\tt else} {\tacexprlow}\\
 & | & {\tacexprlow}\\
 \\
 {\tacexprlow} & ::= &
@@ -467,6 +468,24 @@ applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt
   {\tacexpr}$_2$ {\tt ]} (except that if it fails, it fails like
 $v_2$). Branching is left-associative.
 
+\subsubsection[Generalized biased branching]{Generalized biased branching\tacindex{tryif}
+\index{Tacticals!tryif@{\tt tryif}}}
+
+The tactic
+\begin{quote}
+{\tt if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$}
+\end{quote}
+is a generalization of the biased-branching tactics above. The
+expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied
+to each subgoal independently. For each goal where $v_1$ succeeds at
+least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied
+collectively to the generated subgoals. The $v_2$ tactic can trigger
+backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt
+  if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
+equivalent to $v_1;v_2$. In each of the goals where $v_1$ does not
+succeed at least once, {\tacexpr}$_3$ is evaluated in $v_3$ which is
+is then applied to the goal.
+
 \subsubsection[Soft cut]{Soft cut\tacindex{once}\index{Tacticals!once@{\tt once}}}
 
 Another way of restricting backtracking is to restrict a tactic to a
-- 
cgit v1.2.3


From 3c0e842a133a9da088a9f0fe0fb9b0e699f984ac Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 14 Jan 2015 14:50:31 +0100
Subject: Reference manual: I had previously omitted the syntax entry for [>
 t1|…|tn].

---
 doc/refman/RefMan-ltac.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 73bcc85871..b90e682df1 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -91,6 +91,7 @@ is understood as
 \begin{tabular}{lcl}
 {\tacexpr} & ::= &
            {\tacexpr} {\tt ;} {\tacexpr}\\
+& | & {\tt [>} \nelist{\tacexpr}{|} {\tt ]}\\
 & | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
 & | & {\tacexprpref}\\
 \\
-- 
cgit v1.2.3


From 819f31ec6c8d0b43ac4b62bcecc6b2facbc01a71 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 14 Jan 2015 19:08:37 +0100
Subject: CoqIDE: a Make file to build coqidetop toploop

---
 ide/Make | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 ide/Make

diff --git a/ide/Make b/ide/Make
new file mode 100644
index 0000000000..c0881ca392
--- /dev/null
+++ b/ide/Make
@@ -0,0 +1,6 @@
+interface.mli
+xmlprotocol.mli
+xmlprotocol.ml
+ide_slave.ml
+
+coqidetop.mllib
-- 
cgit v1.2.3


From 8050c90b1cfc755abb16c83df0eebaed85cd67d2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 14 Jan 2015 19:08:55 +0100
Subject: coq_makefile: chmod 755 on toplopp cmxs

---
 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 b73fdba1e6..ac3f6fc8b3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -270,7 +270,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
     if (not_empty cmxsfiles) then begin
       print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
       printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
-      printf "\t install -m 0644 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
+      printf "\t install -m 0755 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
       print "\n";
     end;
     print "install:";
-- 
cgit v1.2.3


From f9aa622d103fbdf620ea2bc3240eafa829e38bcb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 14 Jan 2015 19:09:13 +0100
Subject: Makefile: install ide/*lang

---
 Makefile.build | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index f4b5a63ae1..c415ce1356 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -311,7 +311,7 @@ COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
 .SUFFIXES:.vo
 
-IDEFILES=$(wildcard ide/coq*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
+IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
 
 coqide-binaries: coqide-$(HASCOQIDE)
 coqide-no:
@@ -366,7 +366,7 @@ endif
 
 install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time
 	$(MKDIR) $(FULLDATADIR)
-	$(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $(FULLDATADIR)
+	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR)
 	$(MKDIR) $(FULLCONFIGDIR)
 	if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
 
@@ -395,7 +395,7 @@ $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
 	$(MKDIR) $@/coq/
-	$(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $@/coq/
+	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/
 	$(MKDIR) $@/gtksourceview-2.0/{language-specs,styles}
 	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
 	$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
-- 
cgit v1.2.3


From 071f065b0bf089a5084483fde265fff5ba929f23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Jan 2015 17:54:47 +0100
Subject: Tentatively updating credits while remaining brief.

---
 CREDITS                   | 58 +++++++++++++++++++----------------------------
 doc/refman/RefMan-pre.tex | 19 +++++++++-------
 2 files changed, 34 insertions(+), 43 deletions(-)

diff --git a/CREDITS b/CREDITS
index b05917930b..9a6db78a0c 100644
--- a/CREDITS
+++ b/CREDITS
@@ -1,5 +1,4 @@
 The "Coq proof assistant" was jointly developed by
-
 - INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2 projects
   (starting 1985),
 - Laboratoire de l'Informatique du Parallelisme (LIP)
@@ -27,16 +26,12 @@ the GNU Lesser General Public License Version 2.1.
 
 plugins/cc
   developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
-  University at Nijmegen, 2005-2008)
-plugins/correctness
-  developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
-plugins/dp
-  developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
-  (LRI, 2005-2008)
+  University at Nijmegen, 2005-2008, Grenoble 1, 2010-2014)
+plugins/decl_mode
+  developed by Pierre Corbineau (Radboud University at Nijmegen, 2005-2008,
+  Grenoble 1, 2009-2011)
 plugins/extraction
   developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
-plugins/field
-  developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
 plugins/firstorder
   developed by Pierre Corbineau (LRI, 2003-2008)
 plugins/fourier
@@ -48,10 +43,9 @@ plugins/funind
 plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
 plugins/nsatz
-  developed by Loïc Pottier (INRIA-Marelle, 2009)
-plugins/ring
-  developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
-  Loiseleur (LRI, 1997-1999)
+  developed by Loïc Pottier (INRIA-Marelle, 2009-2011)
+plugins/quote
+  developed by Patrick Loiseleur (LRI, 1997-1999)
 plugins/romega
   developed by Pierre Crégut (France Telecom R&D, 2001-2004)
 plugins/rtauto
@@ -62,51 +56,43 @@ plugins/setoid_ring
   and Bruno Barras (INRIA LogiCal, 2005-2006),
 plugins/subtac
   developed by Matthieu Sozeau (LRI, 2005-2008)
-plugins/xml
-  developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005)
-  as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
-  part of the ProofWeb project (Radboud University at Nijmegen, 2008)
 plugins/micromega
   developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some
   extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
   interface to the csdp solver uses code from John Harrison (University
   of Cambridge, 1998)
-parsing/search.ml
-  mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
 theories/ZArith
   started by Pierre Crégut (France Telecom R&D, 1996)
 theories/Strings
   developed by Laurent Théry (INRIA-Lemme, 2003)
 theories/Numbers/Cyclic
-  developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
+  developed by Benjamin Grégoire (INRIA-Everest, 2007),
+  Laurent Théry (INRIA-Marelle, 2007-2008),
+  Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
 ide/utils
   some files come from Maxence Guesdon's Cameleon tool
 
-Many discussions within the INRIA teams and labs taking part to the
-development influenced the design of Coq especially with
-
-  C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat,
-  S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi,
-  C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas,
-  P.-Y. Strub, L. Théry, B. Werner
+The development of Coq significantly benefited from feedback,
+suggestions or short contributions from the following non exhaustive
+list of persons and groups:
 
-The development of Coq also significantly benefited from feedback,
-suggestions or short contributions from:
-
-  C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
-  P. Castéran (University Bordeaux 1),
+  C. Alvarado, C. Auger, F. Blanqui, P. Castéran, C. Cohen,
+  J. Courant, J. Duprat, F. Garillot, G. Gonthier, J. Goubault,
+  J.-P. Jouannaud, S. Lescuyer, A. Miquel, J.-F. Monin, P.-Y. Strub
   the Foundations Group (Radboud University, Nijmegen, The Netherlands),
   Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
-  F. Garillot, G. Gonthier (INRIA-MSR joint lab),
   INRIA-Gallium project,
   the CS dept at Yale, the CIS dept at U. Penn,
-  the CSE dept at Harvard, the CS dept at Princeton
+  the CSE dept at Harvard, the CS dept at Princeton, the CS dept at MIT
+  as well as a lot of users on coq-club, coqdev, coq-bugs
 
 The following people have contributed to the development of different versions
 of the Coq Proof assistant during the indicated time:
 
   Bruno Barras (INRIA, 1995-now)
+  Yves Bertot (INRIA, 2000-now)
   Pierre Boutillier (INRIA-PPS, 2010-now)
+  Xavier Clerc (INRIA, 2012-2014)
   Jacek Chrzaszcz (LRI, 1998-2003)
   Thierry Coquand (INRIA, 1985-1989)
   Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-2011)
@@ -115,14 +101,16 @@ of the Coq Proof assistant during the indicated time:
   David Delahaye (INRIA, 1997-2002)
   Maxime Dénès (INRIA, 2013-now)
   Daniel de Rauglaudre (INRIA, 1996-1998)
+  Maxime Dénès (INRIA, 2013-now)
   Olivier Desmettre (INRIA, 2001-2003)
   Gilles Dowek (INRIA, 1991-1994)
   Amy Felty (INRIA, 1993)
   Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-2008)
   Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
-  Stéphane Glondu (INRIA-PPS, 2007-now)
+  Stéphane Glondu (INRIA-PPS, 2007-2013)
   Benjamin Grégoire (INRIA, 2003-2011)
   Hugo Herbelin (INRIA, 1996-now)
+  Sébastien Hinderer (INRIA, 2014)
   Gérard Huet (INRIA, 1985-1997)
   Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now)
   Patrick Loiseleur (Paris Sud, 1997-1999)
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 8c169ee1e8..ef7a61931c 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -959,7 +959,7 @@ The way Coq processes a document in batch and interactive mode has
 been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
 proofs, the text between Proof and Qed, can be processed
 asynchronously, decoupling the checking of definitions and statements
-from the checking of proofs.  In interactively this improves the
+from the checking of proofs.  In interactive use, this improves the
 reactiveness of the system, since proofs can be processed in the
 background.  Similarly the compilation of a file can be split into two
 phases:  the first one checking only definitions and statements and
@@ -967,15 +967,18 @@ the second one checking proofs.  A file resulting from the first
 phase, .vio extension, can be already Required.  All .vio files can be
 turned into complete .vo files in parallel.  The same infrastructure
 also allows terminating tactics to be run in parallel on a set of
-goals via the par: goal selector.
-CoqIDE was patched to cope with asynchronous checking of the document.
+goals via the \verb=par:= goal selector.
+
+CoqIDE was modified to cope with asynchronous checking of the document.
 Its source code was also made separate from the one of Coq making it no
 more a special user interface and allowing its release cycle to be
 decoupled with the one of Coq.
-Carst Tankink developed a Coq back end for PIDE enabled user interfaces,
-like PIDE/jEdit (with help from Makarius Wenzel) or PIDE/Coqoon (with
-help from Alexander Faithfull and Jesper Bengtson).
-The development of such features was funded by the Paral-ITP ANR project.
+
+Carst Tankink developed a Coq back end for user interfaces built on
+Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
+help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander
+Faithfull and Jesper Bengtson).  The development of such features was
+funded by the Paral-ITP French ANR project.
 
 The universe polymorphism extension is based on a change of the kernel
 architecture to handle constraint checking only, leaving the generation
@@ -999,7 +1002,7 @@ the relations between homotopy theory and type theory.
 {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
 and improvements regarding the different components of the system.
 
-High-Level Specification Language: 
+High-Level Specification Language:
 - tactics in terms
 - Universe inconsistency and unification error messages
 - Named existentials
-- 
cgit v1.2.3


From 935a2a52dc5ec20f97ea6c002988c6fa292184a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 06:55:01 +0100
Subject: Hugo put me in credits, but I was already there :)

---
 CREDITS | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CREDITS b/CREDITS
index 9a6db78a0c..ace4648dc7 100644
--- a/CREDITS
+++ b/CREDITS
@@ -101,7 +101,6 @@ of the Coq Proof assistant during the indicated time:
   David Delahaye (INRIA, 1997-2002)
   Maxime Dénès (INRIA, 2013-now)
   Daniel de Rauglaudre (INRIA, 1996-1998)
-  Maxime Dénès (INRIA, 2013-now)
   Olivier Desmettre (INRIA, 2001-2003)
   Gilles Dowek (INRIA, 1991-1994)
   Amy Felty (INRIA, 1993)
-- 
cgit v1.2.3


From fa397ec05fdfea053470cddafd1ab09a710f5bc9 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 13 Jan 2015 21:22:54 +0100
Subject: Always build (even when -coqide no) and install idetoploop

So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed)
---
 Makefile.build | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index c415ce1356..0d87d98e96 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -313,11 +313,16 @@ COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
 IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
 
-coqide-binaries: coqide-$(HASCOQIDE)
+coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
 coqide-no:
-coqide-byte: $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA)
-coqide-opt:  $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
+coqide-byte: $(COQIDEBYTE) $(COQIDE)
+coqide-opt:  $(COQIDEBYTE) $(COQIDE)
 coqide-files: $(IDEFILES)
+ifeq ($(BEST),opt)
+ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
+else
+ide-toploop: $(IDETOPLOOPCMA)
+endif
 
 ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
@@ -340,7 +345,7 @@ $(COQIDEBYTE): $(LINKIDE)
 .PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 
 ifeq ($(HASCOQIDE),no)
-install-coqide:
+install-coqide: install-ide-toploop
 else
 install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 endif
-- 
cgit v1.2.3


From 8f077f6d05d0c764e401ce6770f6b598523c33fc Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 13 Jan 2015 23:26:13 +0100
Subject: coq_makefile installs native files

---
 tools/coq_makefile.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ac3f6fc8b3..d877ed564a 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -257,7 +257,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
     let cmxsfiles = List.rev_append cmofiles mllibfiles in
     let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in
     let where_what_oth = vars_to_put_by_root
-      [("VOFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)]
+      [("VOFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)]
       inc in
     let doc_dir = where_put_doc inc in
     let () = if is_install = Project_file.UnspecInstall then
@@ -328,9 +328,7 @@ let clean sds sps =
   end;
   if !some_vfile then
     begin
-      print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native)\n";
-      print "\trm -f $(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo)\n";
-      print "\trm -f $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n";
       print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"
     end;
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
@@ -577,8 +575,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "GFILES:=$(VFILES:.v=.g)\n";
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
       print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
-      print "OBJFILES:=$(call vo_to_obj,$(VOFILES))\n";
-      classify_files_by_root "OBJFILES" l inc
+      print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n";
+      print "NATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      classify_files_by_root "NATIVEFILES" l inc
   end;
   decl_var "ML4FILES" ml4files;
   decl_var "MLFILES" mlfiles;
-- 
cgit v1.2.3


From 530dcf1e6cd008e89a527dacb836202bcb2d02db Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 07:49:27 +0100
Subject: Make installation of native files more robust.

---
 tools/coq_makefile.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d877ed564a..28b86ddc78 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -505,7 +505,7 @@ let parameters () =
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
   print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
   print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
-  print "    $(shell $(COQBIN)coqtop -batch -quiet -print-mod-uid $(vo))))))))\n\n"
+  print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
@@ -576,7 +576,8 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
       print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
       print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n";
-      print "NATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n";
       classify_files_by_root "NATIVEFILES" l inc
   end;
   decl_var "ML4FILES" ml4files;
-- 
cgit v1.2.3


From f7dd427889f3ab966238f9566ec1b5edbd6c6ab6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 07:50:47 +0100
Subject: Mention guard condition in CHANGES.

---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGES b/CHANGES
index 4a9c3a40d8..2088fa6ff7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,6 +35,11 @@ Logic
 - New universe polymorphism.
 - New option -type-in-type to collapse the universe hierarchy (this makes the
   logic inconsistent).
+- The guard condition for fixpoints is now a bit stricter. Propagation of
+subterm value through pattern matching is restricted according to the return
+predicate. Restores compatibility of Coq's logic with the propositional
+extensionality axiom. May create incompatibilities in recursive programs heavily
+using dependent types.
 
 Vernacular commands
 
-- 
cgit v1.2.3


From bdcef127b212f6acd85d4eeb16a008491bd50740 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 07:51:25 +0100
Subject: Mention CHANGES file in COMPATIBILITY.

---
 COMPATIBILITY | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 57553f9e1a..2ce29346c5 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,6 +1,8 @@
 Potential sources of incompatibilities between Coq V8.4 and V8.5
 ----------------------------------------------------------------
 
+(see also file CHANGES)
+
 Universe Polymorphism.
 
 - Refinement, unification and tactics are now aware of universes,
-- 
cgit v1.2.3


From d66b734336cf04a94ac3ef1bd129dfcd3bba92d2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 13:28:21 +0100
Subject: Make -print-mod-uid accept a list of files.

Solves an efficiency problem in Makefiles generated by coq_makefile.
---
 kernel/nativelib.mli  | 3 +++
 tools/coq_makefile.ml | 5 +++++
 toplevel/coqtop.ml    | 9 ++++++---
 3 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index b4a3639f77..0941dc56ce 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -10,6 +10,9 @@ open Nativecode
 (** This file provides facilities to access OCaml compiler and dynamic linker,
 used by the native compiler. *)
 
+(* Directory where compiled files are stored *)
+val output_dir : string
+
 val get_load_paths : (unit -> string list) ref
 
 val load_obj : (string -> unit) ref
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 28b86ddc78..badaf280e4 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -503,9 +503,14 @@ let parameters () =
   print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
   print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
+  print "vo_to_obj = $(addsuffix .o,\\\n";
+  print "  $(filter-out Warning: Error:,\\\n";
+  print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
+(*
   print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
   print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
   print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
+ *)
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9f670c7311..142f338674 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -375,9 +375,12 @@ let schedule_vio_compilation () =
   if !vio_files <> [] && not !vio_checking then
     Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
 
-let print_native_name s =
+let get_native_name s =
   (* We ignore even critical errors because this mode has to be super silent *)
-  try print_endline (Library.native_name_from_filename s) with _ -> ()
+  try
+    String.concat Filename.dir_sep [Filename.dirname s;
+      Nativelib.output_dir; Library.native_name_from_filename s]
+  with _ -> ""
 
 let parse_args arglist =
   let args = ref arglist in
@@ -461,7 +464,7 @@ let parse_args arglist =
     |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ())
     |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
     |"-outputstate" -> set_outputstate (next ())
-    |"-print-mod-uid" -> print_native_name (next ()); exit 0
+    |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
     |"-require" -> add_require (next ())
     |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
-- 
cgit v1.2.3


From 93fa642fa5e4134d034a1f10fe6dffa4a36182cf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 13:32:20 +0100
Subject: Remove left-over dead code in previous commit.

---
 tools/coq_makefile.ml | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index badaf280e4..e9bdb6caca 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -506,11 +506,6 @@ let parameters () =
   print "vo_to_obj = $(addsuffix .o,\\\n";
   print "  $(filter-out Warning: Error:,\\\n";
   print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
-(*
-  print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
-  print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
-  print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
- *)
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
-- 
cgit v1.2.3