Merge branch 'v8.6'

4 files changed, 45 insertions, 28 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d5b125135..468446982 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1934,14 +1934,22 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  *)
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
+  let refresh_tycon sigma t =
+    (** If we put the typing constraint in the term, it has to be
+       refreshed to preserve the invariant that no algebraic universe
+       can appear in the term.  *)
+    refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
+		      env sigma t
+  in
   let preds =
     match pred, tycon with
     (* No return clause *)
     | None, Some t when not (noccur_with_meta 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
-	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let p1 =
+       (* First strategy: we abstract the tycon wrt to the dependencies *)
+         let sigma, t = refresh_tycon sigma t in
+         let p1 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
@@ -1952,7 +1960,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
         let sigma,t = match tycon with
-	| Some t -> sigma,t
+	| Some t -> refresh_tycon sigma t
 	| None -> 
           let sigma = Sigma.Unsafe.of_evar_map sigma in
           let Sigma ((t, _), sigma, _) =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 6bc61f6dd..d8fad1687 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -114,10 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
 
 val prepare_predicate :            Loc.t ->
            (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+            Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
            (Term.types * tomatch_type) list ->
            Context.Rel.t list ->
            Constr.constr option ->
-           'a option -> (Evd.evar_map * Names.name list * Term.constr) list
+           glob_constr option ->
+           (Evd.evar_map * Names.name list * Term.constr) list
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 1ae5532be..92662f07d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,33 +42,39 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-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 ?(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 = 
-    match kind_of_term t with
-    | Sort (Type u as s) when
-      (match Univ.universe_level u with
-      | None -> true
-      | Some l -> not onlyalg && refresh_level evd s) ->
+  (* direction: true for fresh universes lower than the existing ones *)
+  let refresh_sort status ~direction s =
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
-      if dir then set_leq_sort env !evdref s' s
+      if direction then set_leq_sort env !evdref s' s
       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'
+    modified := true; evdref := evd; mkSort s'
+  in
+  let rec refresh ~onlyalg status ~direction t =
+    match kind_of_term t with
+    | Sort (Type u as s) ->
+       (match Univ.universe_level u with
+	| None -> refresh_sort status ~direction s
+	| Some l ->
+	   (match Evd.universe_rigidity evd l with
+	    | UnivRigid ->
+	       if not onlyalg then refresh_sort status ~direction s
+	       else t
+	    | UnivFlexible alg ->
+	       if onlyalg && alg then
+	         (evdref := Evd.make_flexible_variable !evdref false l; t)
+	       else t))
+    | Sort (Prop Pos as s) when refreshset && not direction ->
+       (* Cannot make a universe "lower" than "Set",
+          only refreshing when we want higher universes. *)
+       refresh_sort status ~direction s
     | Prod (na,u,v) -> 
-      mkProd (na,u,refresh status dir v)
+      mkProd (na, u, refresh ~onlyalg status ~direction v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
@@ -81,7 +87,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh univ_flexible true evi.evar_concl in
+      let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
@@ -101,9 +107,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   in
   let t' = 
     if isArity t then
-      (match pbty with
-      | None -> t
-      | Some dir -> refresh status dir t)
+      match pbty with
+      | None ->
+	 (* No cumulativity needed, but we still need to refresh the algebraics *)
+	 refresh ~onlyalg:true univ_flexible ~direction:false t
+      | Some direction -> refresh ~onlyalg status ~direction t
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a85e493ea..1fdbbb412 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1266,7 +1266,7 @@ let sigma_compare_sorts env pb s0 s1 sigma =
   match pb with
   | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
-    
+
 let sigma_compare_instances ~flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
   with Evd.UniversesDiffer