Merge branch 'v8.5'

16 files changed, 137 insertions, 15 deletions

diff --git a/CHANGES b/CHANGES
index 91d5f0baa6..9108c14543 100644
--- a/CHANGES
+++ b/CHANGES
@@ -89,6 +89,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
 ===================================
 
@@ -418,6 +425,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).
diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
new file mode 100755
index 0000000000..a8b5d10dad
--- /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 -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
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/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 =
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 3f9ac87a6e..5f657aff57 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/pretyping/unification.ml b/pretyping/unification.ml
index 269c723e30..e8a0df4844 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -920,8 +920,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
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d69b5b4215..f629539079 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1045,10 +1045,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/tactics/rewrite.ml b/tactics/rewrite.ml
index d1b14e3d99..9a19d4bda7 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1509,7 +1509,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 { run = begin fun sigma ->
@@ -2081,8 +2081,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.
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.
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
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
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.
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.