Merge branch 'v8.5'

5 files changed, 24 insertions, 9 deletions

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