Avoid introducing additional universes when doing pruning in evarsolve.

2 files changed, 12 insertions, 12 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 5f19ce30a..08b704bde 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -47,7 +47,7 @@ let get_polymorphic_positions f =
    hd ?A (l : list t) -> A = t
 
 *)
-let refresh_universes ?(onlyalg=false) pbty env evd t =
+let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh dir t = 
@@ -56,15 +56,15 @@ let refresh_universes ?(onlyalg=false) pbty env evd t =
       (match Univ.universe_level u with
       | None -> true 
       | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) ->
-      (* s' will appear in the term, it can't be algebraic *)
-      let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in
-      let evd = 
-	if dir then set_leq_sort !evdref s' s
-	else set_leq_sort !evdref s s'
-      in
-	modified := true; evdref := evd; mkSort 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 evd = 
+      if dir then set_leq_sort !evdref s' s
+      else set_leq_sort !evdref s s'
+    in
+      modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
-      mkProd (na,u,refresh dir v)
+    mkProd (na,u,refresh dir v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars t =
@@ -561,7 +561,7 @@ 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 (Some false) env evd (mkSort s) in
+        let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
         define_evar_from_virtual_equation define_fun env evd t_in_env 
           ty_t_in_sign sign filter inst_in_env in
       let evd,b_in_sign = match b with
@@ -580,7 +580,7 @@ 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 (Some false) env evd (mkSort s) in
+    let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd 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 16a4aff5b..e35fb44b1 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,7 +34,7 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) ->
+val refresh_universes : ?inferred:bool -> ?onlyalg:bool (* Only algebraic universes *) ->
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types