Merge branch 'v8.5' into v8.6

18 files changed, 289 insertions, 70 deletions

diff --git a/.mailmap b/.mailmap
index 13c71558f..51c8778f8 100644
--- a/.mailmap
+++ b/.mailmap
@@ -52,6 +52,7 @@ Pierre Letouzey <pierre.letouzey@inria.fr>         letouzey <letouzey@85f007b7-5
 Assia Mahboubi <assia.mahboubi@inria.fr>           amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Evgeny Makarov <emakarov@gforge>                   emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Gregory Malecha <gmalecha@eecs.harvard.edu>        Gregory Malecha <gmalecha@cs.harvard.edu>
+Gregory Malecha <gmalecha@eecs.harvard.edu>        Gregory Malecha <gmalecha@gmail.com>
 Lionel Elie Mamane <lmamane@gforge>                lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Claude Marché <marche@gforge>                      marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Micaela Mayero <mayero@gforge>                     mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7>
@@ -69,6 +70,8 @@ Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-54
 Loïc Pottier <pottier@gforge>                      pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Matthias Puech <puech@gforge>                      puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>  regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr>
+Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@gforge>
 Clément Renard <clrenard@gforge>                   clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Claudio Sacerdoti Coen <sacerdot@gforge>           sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Vincent Siles <vsiles@gforge>                      vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7>
@@ -79,7 +82,8 @@ Arnaud Spiwack <arnaud@spiwack.net>                aspiwack <aspiwack@85f007b7-5
 Enrico Tassi <Enrico.Tassi@inria.fr>               gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
 Enrico Tassi <Enrico.Tassi@inria.fr>               Enrico Tassi <enrico.tassi@inria.fr>
 Enrico Tassi <Enrico.Tassi@inria.fr>               Enrico Tassi <gares@fettunta.org>
-Laurent Théry <thery@gforge>                       thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Laurent Théry <laurent.thery@inria.fr>             thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7>
+Laurent Théry <laurent.thery@inria.fr>             thery <thery@sophia.inria.fr>
 Benjamin Werner <werner@gforge>                    werner <werner@85f007b7-540e-0410-9357-904b9bb8a0f7>
 
 # Anonymous accounts
diff --git a/CHANGES b/CHANGES
index 7956db6f5..c25649823 100644
--- a/CHANGES
+++ b/CHANGES
@@ -105,6 +105,7 @@ Other bugfixes
 - #4882: anomaly with Declare Implicit Tactic on hole of type with evars
 - Fix use of "Declare Implicit Tactic" in refine.
   triggered by CoqIDE
+- #4069, #4718: congruence fails when universes are involved.
 
 Universes
 - Disallow silently dropping universe instances applied to variables
diff --git a/configure.ml b/configure.ml
index 06d8e713b..c8096b9e0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -13,7 +13,7 @@ open Printf
 
 let coq_version = "trunk"
 let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of
-three non-negative, period-separed integers [...]" *)
+three non-negative, period-separated integers [...]" *)
 let vo_magic = 8511
 let state_magic = 58511
 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
@@ -934,7 +934,7 @@ let print_summary () =
   pr "\n";
   pr "  Architecture                : %s\n" arch;
   if operating_system <> "" then
-    pr "  Operating system          : %s\n" operating_system;
+    pr "  Operating system            : %s\n" operating_system;
   pr "  Coq VM bytecode link flags  : %s\n" (String.concat " " vmbyteflags);
   pr "  Other bytecode link flags   : %s\n" custom_flag;
   pr "  OS dependent libraries      : %s\n" osdeplibs;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 23c0c1c31..09f7bd75c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -851,6 +851,9 @@ let export ?except senv dir =
 let import lib cst vodigest senv =
   check_required senv.required lib.comp_deps;
   check_engagement senv.env lib.comp_enga;
+  if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then
+    CErrors.errorlabstrm "Safe_typing.import"
+     (Pp.strbrk "Cannot load a library with the same name as the current one.");
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
   let env = Environ.push_context_set ~strict:true
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index aff60eaa4..fd46d8069 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -82,8 +82,10 @@ let rec decompose_term env sigma t=
     | Proj (p, c) -> 
 	let canon_const kn = constant_of_kn (canonical_con kn) in 
 	let p' = Projection.map canon_const p in
-	  (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
-    | _ ->if closed0 t then (Symb t) else raise Not_found
+	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
+    | _ ->
+       let t = strip_outer_cast t in
+       if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
 open Globnames
@@ -233,10 +235,10 @@ let build_projection intype (cstr:pconstructor) special default gls=
 
 let _M =mkMeta
 
-let app_global f args k = 
+let app_global f args k =
   Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
-let new_app_global f args k = 
+let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
@@ -246,7 +248,19 @@ let assert_before n c =
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end }
-    
+
+let refresh_type env evm ty =
+  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
+			      (Some false) env evm ty
+
+let refresh_universes ty k =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let evm = Tacmach.New.project gl in
+    let evm, ty = refresh_type env evm ty in
+    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
+  end }
+
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
@@ -256,35 +270,31 @@ let rec proof_tac p : unit Proofview.tactic =
     | SymAx c ->
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
-        let typ = (* Termops.refresh_universes *) type_of l in
-        new_app_global _sym_eq [|typ;r;l;c|] exact_check
+	refresh_universes (type_of l) (fun typ ->
+        new_app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
 	let lr = constr_of_term t in
-	let typ = (* Termops.refresh_universes *) type_of lr in
-        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check
+	refresh_universes (type_of lr) (fun typ ->
+        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = (* Termops.refresh_universes *) (type_of t2) in
+	refresh_universes (type_of t2) (fun typ ->
 	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
-          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]
+          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	and tx1=constr_of_term p2.p_lhs
 	and tf2=constr_of_term p1.p_rhs
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = (* Termops.refresh_universes  *)(type_of tf1) in
-	let typx = (* Termops.refresh_universes *) (type_of tx1) in
-	let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in
+	refresh_universes (type_of tf1) (fun typf ->
+	refresh_universes (type_of tx1) (fun typx ->
+	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1 =
-	  app_global _f_equal
-		[|typf;typfx;appx1;tf1;tf2;_M 1|] in
-	let lemma2=
-	  app_global _f_equal
-		[|typx;typfx;tf2;tx1;tx2;_M 1|] in
+	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
+	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
 	let prf =
 	  app_global _trans_eq
 		[|typfx;
@@ -298,34 +308,33 @@ let rec proof_tac p : unit Proofview.tactic =
 		reflexivity;
                 Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")]]
+		       "I don't know how to handle dependent equality")]])))
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype = (* Termops.refresh_universes *) (type_of ti) in
-	 let outtype = (* Termops.refresh_universes *) (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
+	 refresh_universes (type_of ti) (fun intype ->
+         refresh_universes (type_of default) (fun outtype ->
          let proj =
            Tacmach.New.of_old (build_projection intype cstr special default) gl
          in
 	 let injt=
            app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end }
 
 let refute_tac c t1 t2 p =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
-  in
-  let neweq= new_app_global _eq [|intype;tt1;tt2|] in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
+  let k intype =
+    let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end }
 
 let refine_exact_check c gl =
@@ -335,16 +344,15 @@ let refine_exact_check c gl =
 let convert_to_goal_tac c t1 t2 p = 
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
-  in
-  let neweq= new_app_global _eq [|sort;tt1;tt2|] in
-  let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
-  let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-  let identity=mkLambda (Name x,sort,mkRel 1) in
-  let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+  let k sort =
+    let neweq= new_app_global _eq [|sort;tt1;tt2|] in
+    let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
+    let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let identity=mkLambda (Name x,sort,mkRel 1) in
+    let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
-      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -360,33 +368,28 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
 let discriminate_tac (cstr,u as cstru) p =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-    let intype =
-      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
-    in
+    let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
-    (* let outsort = mkSort outsort in *)
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-    (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
-    (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
     let identity = Universes.constr_of_global (Lazy.force _I) in
-    (* let trivial=pf_unsafe_type_of gls identity in *)
     let trivial = Universes.constr_of_global (Lazy.force _True) in
-    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in 
+    let evm = Tacmach.New.project gl in
+    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
+    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
-    let pred=mkLambda(Name xid,outtype,mkRel 1) in
+    let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
     let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
     let injt=app_global _f_equal
-                    [|intype;outtype;proj;t1;t2;mkVar hid|] in
+			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
-        app_global _eq_rect
-          [|outtype;trivial;pred;identity;concl;injt|] k) in
+            app_global _eq_rect
+		       [|outtype;trivial;pred;identity;concl;injt|] k) in
     let neweq=new_app_global _eq [|intype;t1;t2|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
-      (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-        [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
+			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
   end }
 
 (* wrap everything *)
@@ -470,7 +473,7 @@ let congruence_tac depth l =
    This isn't particularly related with congruence, apart from
    the fact that congruence is called internally.
 *)
-    
+
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -482,7 +485,7 @@ let mk_eq f c1 c2 k =
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
     end })
-    
+
 let f_equal =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 3068b5347..b11d15e5c 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -298,7 +298,9 @@ Ltac nsatz_call_n info nparam p rr lp kont :=
   match goal with
   | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ =>
     intros _;
+    let lci := fresh "lci" in
     set (lci:=lci0);
+    let lq := fresh "lq" in
     set (lq:=lq0);
     kont c rr lq lci
   end.
@@ -380,10 +382,13 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
     end in 
 
   SplitPolyList ltac:(fun p lp =>
+    let p21 := fresh "p21" in
+    let lp21 := fresh "lp21" in
     set (p21:=p) ;
     set (lp21:=lp);
 (*    idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *)
     nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => 
+      let q := fresh "q" in
       set (q := PEmul c (PEpow p21 r)); 
       let Hg := fresh "Hg" in 
       assert (Hg:check lp21 q (lci,lq) = true); 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 338ac4300..6c8677855 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -47,7 +47,8 @@ let refresh_level evd s =
   | None -> true
   | Some l -> not (Evd.is_flexible_level evd l)
 
-let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
+		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh status dir t = 
@@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
       else set_leq_sort env !evdref s s'
     in
       modified := true; evdref := evd; mkSort s'
+    | Sort (Prop Pos as s) when refreshset && not dir ->
+       let s' = evd_comb0 (new_sort_variable status) evdref in
+       let evd = set_leq_sort env !evdref s s' in
+       modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
       mkProd (na,u,refresh status dir v)
     | _ -> t
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 918ba12f0..f94c83b6d 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,8 +34,12 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : ?status:Evd.rigid ->
-			?onlyalg:bool (* Only algebraic universes *) ->
+val refresh_universes :
+  ?status:Evd.rigid ->
+  ?onlyalg:bool (* Only algebraic universes *) ->
+  ?refreshset:bool ->
+  (* Also refresh Prop and Set universes, so that the returned type can be any supertype
+     of the original type *)
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 21b03ce54..61527764e 100644
--- a/test-suite/bugs/closed/4069.v
+++ b/test-suite/bugs/closed/4069.v
@@ -49,3 +49,56 @@ Lemma bar {A} n m (x : A) :
   skipn n (replicate m x) = replicate (m - n) x.
 Proof. intros. f_equal.
 (* 8.5: one goal, n = m - n *)
+Abort.
+
+Variable F : nat -> Set.
+Variable X : forall n, F (n + 1).
+
+Definition sequator{X Y: Set}{eq:X=Y}(x:X) : Y := eq_rec _ _ x _ eq.
+Definition tequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq.
+Polymorphic Definition pequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq.
+
+Goal {n:nat & F (S n)}.
+eexists.
+unshelve eapply (sequator (X _)).
+f_equal. (*behaves*)
+Undo 2.
+unshelve eapply (pequator (X _)).
+f_equal. (*behaves*)
+Undo 2.
+unshelve eapply (tequator (X _)).
+f_equal. (*behaves now *)
+Focus 2. exact 0.
+simpl.
+reflexivity.
+Defined.
+
+(* Part 2: modulo casts introduced by refine due to reductions in goals *)
+
+Goal {n:nat & F (S n)}.
+eexists.
+(*misbehaves, although same goal as above*)
+Set Printing All.
+unshelve refine (sequator (X _)); revgoals.
+2:exact 0. reflexivity.
+Undo 3. 
+unshelve refine (pequator (X _)); revgoals.
+f_equal.
+Undo 2.
+unshelve refine (tequator (X _)); revgoals.
+f_equal.
+Admitted.
+
+Goal @eq Set nat nat.
+congruence.
+Qed.
+
+Goal @eq Type nat nat.
+congruence. 
+Qed.
+
+Variable T : Type.
+
+Goal @eq Type T T.
+congruence.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v
new file mode 100644
index 000000000..9c0bed42c
--- /dev/null
+++ b/test-suite/bugs/closed/4684.v
@@ -0,0 +1,32 @@
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
+
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
new file mode 100644
index 000000000..ac0653492
--- /dev/null
+++ b/test-suite/bugs/closed/4733.v
@@ -0,0 +1,52 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
+
+(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+
+Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
+(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
new file mode 100644
index 000000000..3ca5c095f
--- /dev/null
+++ b/test-suite/bugs/opened/4803.v
@@ -0,0 +1,34 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
+
+(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *)
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 297ac255d..75dd38fde 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index dc0527d82..bbfe5ec42 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -136,3 +136,18 @@ Inductive I : nat -> Type := C : I 0 | D : I 0.
 Goal ~C=D.
 congruence.
 Qed.
+
+(* Example by Jonathan Leivant, congruence up to universes *)
+Section JLeivant.
+  Variables S1 S2 : Set.
+
+  Definition T1 : Type := S1.
+  Definition T2 : Type := S2.
+
+  Goal T1 = T1.
+    congruence.
+    Undo.
+    unfold T1.
+    congruence.
+  Qed.
+End JLeivant.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 39bc59a65..21b78b533 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -70,3 +70,9 @@ Coercion sigT_of_sig : sig >-> sigT.
 Coercion sig_of_sigT : sigT >-> sig.
 Coercion sigT2_of_sig2 : sig2 >-> sigT2.
 Coercion sig2_of_sigT2 : sigT2 >-> sig2.
+
+(** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5.  This is necessary.  These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *)
+Require Coq.Lists.List.
+Require Coq.Vectors.VectorDef.
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
+Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 9a227ad13..3c5690a72 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -24,6 +24,8 @@ Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
+Notation option_map := option_map (compat "8.4").
+
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
 
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c86253477..b86df7c80 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -465,10 +465,10 @@ let implicit () =
   in
   let v_rules () =
     print "$(VOFILES): %.vo: %.v\n";
-    print "\t$(SHOW)COQC $*\n";
-    print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
-    print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
-    print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n";
+    print "\t$(SHOW)COQC $<\n";
+    print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
+    print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
+    print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n";
     print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n";
     print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
     print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
@@ -477,7 +477,7 @@ let implicit () =
     print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n";
     print "\t$(SHOW)'COQDEP $<'\n";
     print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
-    print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
+    print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n"
   in
     if !some_mlifile then mli_rules ();
     if !some_ml4file then ml4_rules ();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 0559934ec..f83ada466 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -179,7 +179,7 @@ let display_cmd_header loc com =
      str " [" ++ str cmd ++ str "] ")
 
 
-let rec vernac_com verbose checknav (loc,com) =
+let rec vernac_com checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -193,7 +193,7 @@ let rec vernac_com verbose checknav (loc,com) =
           end;
 	begin
 	  try
-            read_vernac_file verbosely f;
+            Flags.silently (read_vernac_file verbosely) f;
 	    restore_translator_coqdoc st;
 	  with reraise ->
             let reraise = CErrors.push reraise in
@@ -203,7 +203,7 @@ let rec vernac_com verbose checknav (loc,com) =
 
     | v when !just_parsing -> ()
 
-    | v -> Stm.interp verbose (loc,v)
+    | v -> Stm.interp (Flags.is_verbose()) (loc,v)
   in
     try
       checknav loc com;
@@ -232,7 +232,7 @@ and read_vernac_file verbosely s =
     while true do
       let loc_ast = parse_sentence input in
       CWarnings.set_current_loc (fst loc_ast);
-      vernac_com verbosely checknav loc_ast
+      vernac_com checknav loc_ast;
     done
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
@@ -256,7 +256,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
+let eval_expr loc_ast = vernac_com checknav loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()