Refresh rigid universes as well, and in 8.4 compatibility mode,

make them rigid to disallow minimization.

3 files changed, 28 insertions, 9 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f06207c3b..3c3720388 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,11 +42,15 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-(**
-   forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed
-   hd ?A (l : list t) -> A = t
+let default_universe_status u =
+  if Flags.version_less_or_equal Flags.V8_4 then univ_rigid
+  else u
+
+let refresh_level evd s =
+  match Evd.is_sort_variable evd s with
+  | None -> true
+  | Some l -> not (Evd.is_flexible_level evd l)
 
-*)
 let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
@@ -54,10 +58,10 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     match kind_of_term t with
     | Sort (Type u as s) when
       (match Univ.universe_level u with
-      | None -> true 
-      | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) ->
+      | None -> true
+      | Some l -> not onlyalg && refresh_level evd s) ->
     let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in
-    let s' = evd_comb0 (new_sort_variable status) evdref in
+    let s' = evd_comb0 (new_sort_variable (default_universe_status status)) evdref in
     let evd = 
       if dir then set_leq_sort env !evdref s' s
       else set_leq_sort env !evdref s s'
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d3d6901b6..b27803bd0 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -715,7 +715,8 @@ let define_pure_evar_as_product evd evk =
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
   let concl = whd_betadeltaiota evenv evd evi.evar_concl in
   let s = destSort concl in
-  let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+  let evd1,(dom,u1) =
+    new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
@@ -724,8 +725,9 @@ let define_pure_evar_as_product evd evk =
        (* Impredicative product, conclusion must fall in [Prop]. *)
         new_evar newenv evd1 concl ~src ~filter
       else
+	let status = univ_flexible_alg in
 	let evd3, (rng, srng) =
-	  new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
+	  new_type_evar newenv evd1 status ~src ~filter in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
 	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
 	  evd3, rng
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
new file mode 100644
index 000000000..751f1e697
--- /dev/null
+++ b/test-suite/bugs/closed/4394.v
@@ -0,0 +1,13 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Require Import Equality List.
+Unset Strict Universe Declaration.
+Inductive Foo I A := foo (B : Type) : A -> I B -> Foo I A.
+Definition Family := Type -> Type.
+Definition fooFamily family : Family := Foo family.
+Inductive Empty {T} : T -> Prop := .
+Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
+  Empty (a, b) -> False.
+Proof.
+  intro e.
+  dependent induction e.
+Qed.
\ No newline at end of file