From 701a69732ef2abfc7384296e090a3e9bd7604bbd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Nov 2015 18:45:32 +0100
Subject: Fixing bug #3554: Anomaly: Anonymous implicit argument.

We just handle unnamed implicits using a dummy name. Note that the implicit
argument logic should still output warnings whenever the user writes implicit
arguments that won't be taken into account, but I'll leave that for another
time.
---
 interp/constrintern.ml        | 2 +-
 test-suite/bugs/closed/3554.v | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/3554.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c754f1910c..8afe630ec5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -317,7 +317,7 @@ let rec it_mkGLambda loc2 env body =
 let build_impls = function
   |Implicit -> (function
 		  |Name id ->  Some (id, Impargs.Manual, (true,true))
-		  |Anonymous -> anomaly (Pp.str "Anonymous implicit argument"))
+		  |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
   |Explicit -> fun _ -> None
 
 let impls_type_list ?(args = []) =
diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v
new file mode 100644
index 0000000000..13a79cc840
--- /dev/null
+++ b/test-suite/bugs/closed/3554.v
@@ -0,0 +1 @@
+Example foo (f : forall {_ : Type}, Type) : Type.
-- 
cgit v1.2.3


From 2f56f0fcf21902bb1317f1d6f7ba4b593d712646 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 16:04:43 -0500
Subject: Fix bug #4293: ensure let-ins do not contain algebraic universes in
 their type annotation.

---
 pretyping/evarsolve.ml        | 10 ++++++----
 pretyping/evarsolve.mli       |  3 ++-
 pretyping/pretyping.ml        |  4 +++-
 test-suite/bugs/closed/4293.v |  7 +++++++
 4 files changed, 18 insertions(+), 6 deletions(-)
 create mode 100644 test-suite/bugs/closed/4293.v

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 35bc1de593..aeb2445d1c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -47,7 +47,7 @@ let refresh_level evd s =
   | None -> true
   | Some l -> not (Evd.is_flexible_level evd l)
 
-let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh status dir t = 
@@ -98,7 +98,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     if isArity t then
       (match pbty with
       | None -> t
-      | Some dir -> refresh univ_rigid dir t)
+      | Some dir -> refresh status dir t)
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
@@ -609,7 +609,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       let id = next_name_away na avoid in
       let evd,t_in_sign =
         let s = Retyping.get_sort_of env evd t_in_env in
-        let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
+        let evd,ty_t_in_sign = refresh_universes
+	 ~status:univ_flexible (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd src t_in_env
           ty_t_in_sign sign filter inst_in_env in
       let evd,b_in_sign = match b with
@@ -627,7 +628,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
-    let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
+    let evd,ty_t_in_sign = refresh_universes
+     ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd,ev2_in_sign =
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 21d976091f..86a1e3e0ce 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,7 +34,8 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : ?inferred:bool -> ?onlyalg:bool (* Only algebraic universes *) ->
+val refresh_universes : ?status:Evd.rigid ->
+			?onlyalg:bool (* Only algebraic universes *) ->
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d354a6c3c4..dd4fcf1981 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -739,7 +739,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	  pretype (mk_tycon tj.utj_val) env evdref lvar c
       | _ -> pretype empty_tycon env evdref lvar c1
     in
-    let t = j.uj_type in
+    let t = evd_comb1 (Evarsolve.refresh_universes
+      ~onlyalg:true ~status:Evd.univ_flexible (Some false) env)
+      evdref j.uj_type in
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v
new file mode 100644
index 0000000000..3671c931b7
--- /dev/null
+++ b/test-suite/bugs/closed/4293.v
@@ -0,0 +1,7 @@
+Module Type Foo.
+Definition T := let X := Type in Type.
+End Foo.
+
+Module M : Foo.
+Definition T := let X := Type in Type.
+End M.
\ No newline at end of file
-- 
cgit v1.2.3


From ca30a8be08beeae77d42b6cb5d9f219e3932a3f7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:12:39 -0500
Subject: Fix bug #3257, setoid_reflexivity should fail if not completing the
 goal.

---
 tactics/rewrite.ml            | 6 ++++--
 test-suite/bugs/closed/3257.v | 5 +++++
 2 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/3257.v

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index e8a7c0f600..af6953bf85 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -2077,8 +2077,10 @@ let poly_proof getp gett env evm car rel =
 let setoid_reflexivity =
   setoid_proof "reflexive"
     (fun env evm car rel -> 
-      tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof
-		  env evm car rel) (fun c -> Proofview.V82.of_tactic (apply c)))
+     tac_open (poly_proof PropGlobal.get_reflexive_proof
+			  TypeGlobal.get_reflexive_proof
+			  env evm car rel)
+	      (fun c -> tclCOMPLETE (Proofview.V82.of_tactic (apply c))))
     (reflexivity_red true)
 
 let setoid_symmetry =
diff --git a/test-suite/bugs/closed/3257.v b/test-suite/bugs/closed/3257.v
new file mode 100644
index 0000000000..d8aa6a0479
--- /dev/null
+++ b/test-suite/bugs/closed/3257.v
@@ -0,0 +1,5 @@
+Require Import Setoid Morphisms Basics.
+Lemma foo A B (P : B -> Prop) :
+  pointwise_relation _ impl (fun z => A -> P z) P.
+Proof.
+  Fail reflexivity.
-- 
cgit v1.2.3


From 67da4b45ef65db59b2d7ba1549351d792e1b27d9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:15:37 -0500
Subject: Fix bug #3735: interpretation of "->" in Program follows the standard
 one.

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

diff --git a/CHANGES b/CHANGES
index 7b50dfae56..f67c34b81b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -397,6 +397,9 @@ Program
 - "Solve Obligations using" changed to "Solve Obligations with",
   consistent with "Proof with".
 - Program Lemma, Definition now respect automatic introduction.
+- Program Lemma, Definition, etc.. now interpret "->" like Lemma and
+  Definition as a non-dependent arrow (potential source of
+  incompatibility).
 - Add/document "Set Hide Obligations" (to hide obligations in the final
   term inside an implicit argument) and "Set Shrink Obligations" (to
   minimize dependencies of obligations defined by tactics).
-- 
cgit v1.2.3


From a3f0a0daf58964a54b1e6fb1f8252f68a8c9c8ea Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:47:39 -0500
Subject: Fix bug #3998: when using typeclass resolution for conversion, allow
 only one disjoint component of the typeclasses instances to resolve.

---
 pretyping/coercion.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e61e52c178..3163ac0e6e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -343,7 +343,7 @@ let coerce_itf loc env evd v t c1 =
 
 let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
-    ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
+    ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
 
 (* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
-- 
cgit v1.2.3


From 834876a3e07fe8053aa99655f21883c3e8927a8c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 6 Nov 2015 17:52:53 -0500
Subject: Ensure that conversion is called on terms of the same type in
 unification (not necessarily preserved due to the fo approximation rule).

---
 pretyping/unification.ml | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 24e06007e9..9758aa43c4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -904,8 +904,18 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       match subst_defined_metas_evars subst cN with
       | None -> (* some undefined Metas in cN *) None
       | Some n1 ->
-          (* No subterm restriction there, too much incompatibilities *)
-	  let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
+         (* No subterm restriction there, too much incompatibilities *)
+	 let sigma =
+	   if opt.with_types then
+	     try (* Ensure we call conversion on terms of the same type *)
+	       let tyM = get_type_of curenv ~lax:true sigma m1 in
+	       let tyN = get_type_of curenv ~lax:true sigma n1 in
+	       check_compatibility curenv CUMUL flags substn tyM tyN
+	     with RetypeError _ ->
+	       (* Renounce, maybe metas/evars prevents typing *) sigma
+	   else sigma
+	 in 
+	 let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
 	    if b then Some (sigma, metasubst, evarsubst)
 	    else 
 	      if is_ground_term sigma m1 && is_ground_term sigma n1 then
-- 
cgit v1.2.3


From 7de9c1a45a354676a073e216f42c34820e454691 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 11 Nov 2015 20:39:41 +0100
Subject: Now closed.

---
 test-suite/bugs/opened/3554.v | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 test-suite/bugs/opened/3554.v

diff --git a/test-suite/bugs/opened/3554.v b/test-suite/bugs/opened/3554.v
deleted file mode 100644
index 422c5770ea..0000000000
--- a/test-suite/bugs/opened/3554.v
+++ /dev/null
@@ -1 +0,0 @@
-Fail Example foo (f : forall {_ : Type}, Type) : Type.
-- 
cgit v1.2.3


From 7978e1dbd6dcd409b0b98a4b407a66b104dff3ba Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 12 Nov 2015 11:59:33 +0100
Subject: Script building MacOS package.

---
 dev/make-macos-dmg.sh | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100755 dev/make-macos-dmg.sh

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
new file mode 100755
index 0000000000..8f6a7f9e1b
--- /dev/null
+++ b/dev/make-macos-dmg.sh
@@ -0,0 +1,31 @@
+#!/bin/bash
+
+# Fail on first error
+set -e
+
+# Configuration setup
+eval `opam config env`
+make distclean
+OUTDIR=$PWD/_install
+DMGDIR=$PWD/_dmg
+./configure -debug -prefix $OUTDIR
+VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
+APP=bin/CoqIDE_${VERSION}.app
+
+# Create a .app file with CoqIDE
+~/.local/bin/jhbuild run make -j -l2 $APP
+
+# Build Coq and run test-suite
+make && make check
+
+# Add Coq to the .app file
+make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
+
+# Sign the .app file
+codesign -f -s - $APP
+
+# Create the dmg bundle
+mkdir $DMGDIR
+ln -s /Applications $DMGDIR
+cp -r $APP $DMGDIR
+hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
-- 
cgit v1.2.3


From 69ed7f0ac9d651eaab85153ea55f5c7d9bf6ae20 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 11 Nov 2015 18:14:40 -0500
Subject: Update CHANGES

Mention compatibility file.
---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGES b/CHANGES
index f67c34b81b..719be44929 100644
--- a/CHANGES
+++ b/CHANGES
@@ -68,6 +68,13 @@ Tools
   path of a given library rather than a physical path, thus they behave like
   Require [Import] path.
 
+Standard Library
+
+ - There is now a Coq.Compat.Coq84 library, which sets the various compatibility
+   options and does a few redefinitions to make Coq behave more like Coq v8.4.
+   The standard way of putting Coq in v8.4 compatibility mode is to pass the command
+   line flags "-require Coq.Compat.Coq84 -compat 8.4".
+
 Changes from V8.5beta1 to V8.5beta2
 ===================================
 
-- 
cgit v1.2.3


From db002583b18c8742c0cd8e1a12305166b6b791ce Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Nov 2015 12:05:00 +0100
Subject: Fixed test-suite file for bug #3998.

---
 test-suite/bugs/closed/3998.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/3998.v

diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v
new file mode 100644
index 0000000000..ced13839dd
--- /dev/null
+++ b/test-suite/bugs/closed/3998.v
@@ -0,0 +1,24 @@
+Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }.
+Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *)
+
+Inductive I1 := C.
+Inductive I2 := .
+
+Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }.
+Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }.
+
+Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f.
+
+Class MapOps (M K : Set) := {
+  tgtTy: K -> Set;
+  update: M -> forall k:K, tgtTy k -> M
+}.
+
+Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F :=
+{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }.
+
+Axiom ex : RecordOf _ I1FieldType.
+
+Definition works := (fun ex' => update ex' C true) (update ex C false).
+Set Typeclasses Debug.
+Definition doesnt := update (update ex C false) C true.
\ No newline at end of file
-- 
cgit v1.2.3


From 0c11bc39927c7756a0e3c3a6c445f20d0daaad7f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Nov 2015 14:14:38 +0100
Subject: Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.

We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
---
 proofs/proofview.ml           | 26 +++++++++++++++++++++++++-
 test-suite/bugs/closed/4412.v |  4 ++++
 2 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4412.v

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 4fc0c164e3..59a64658dc 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1010,10 +1010,34 @@ end
 module Refine =
 struct
 
+  let extract_prefix env info =
+    let ctx1 = List.rev (Environ.named_context env) in
+    let ctx2 = List.rev (Evd.evar_context info) in
+    let rec share l1 l2 accu = match l1, l2 with
+    | d1 :: l1, d2 :: l2 ->
+      if d1 == d2 then share l1 l2 (d1 :: accu)
+      else (accu, d2 :: l2)
+    | _ -> (accu, l2)
+    in
+    share ctx1 ctx2 []
+
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
+    (** Typecheck the hypotheses. *)
+    let type_hyp (sigma, env) (na, body, t as decl) =
+      let evdref = ref sigma in
+      let _ = Typing.sort_of env evdref t in
+      let () = match body with
+      | None -> ()
+      | Some body -> Typing.check env evdref body t
+      in
+      (!evdref, Environ.push_named decl env)
+    in
+    let (common, changed) = extract_prefix env info in
+    let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+    let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
+    (** Typecheck the conclusion *)
     let evdref = ref sigma in
-    let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
     let _ = Typing.sort_of env evdref (Evd.evar_concl info) in
     !evdref
 
diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v
new file mode 100644
index 0000000000..4b2aae0c7b
--- /dev/null
+++ b/test-suite/bugs/closed/4412.v
@@ -0,0 +1,4 @@
+Require Import Coq.Bool.Bool Coq.Setoids.Setoid.
+Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True.
+  intros.
+  Fail rewrite Bool.andb_true_iff in H.
-- 
cgit v1.2.3


From 2fd497d380de998c4b22b9f7167eb4023e4cd576 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 13 Nov 2015 14:21:01 +0100
Subject: MacOS package script: do not fail if directory _dmg already exists.

---
 dev/make-macos-dmg.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 8f6a7f9e1b..a8b5d10dad 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -25,7 +25,7 @@ make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq insta
 codesign -f -s - $APP
 
 # Create the dmg bundle
-mkdir $DMGDIR
+mkdir -p $DMGDIR
 ln -s /Applications $DMGDIR
 cp -r $APP $DMGDIR
 hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
-- 
cgit v1.2.3


From 3aeb18bf1412a27309c39713e05eca2c27706ca8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 13 Nov 2015 16:33:26 +0100
Subject: Continue fix of PMP, handling setoid_rewrite in let-bound hyps
 correctly.

---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index af6953bf85..182c232ae9 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1505,7 +1505,7 @@ let assert_replacing id newt tac =
     let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in
     let nc = match before with
     | [] -> assert false
-    | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem
+    | (id, b, _) :: rem -> insert_dependent env (id, None, newt) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Proofview.Refine.refine ~unsafe:false begin fun sigma ->
-- 
cgit v1.2.3