From 14ae5f4534ee5e632d82990e7db76305b9ca9b75 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 21 Jun 2014 16:14:59 +0200
Subject: - Add an option to refresh only algebraic universes, for e_type_of.
 The goal there is not the same as in Evd.define. - Fixed bugs #3330 and
 #3331.

---
 pretyping/evarsolve.ml  | 4 ++--
 pretyping/evarsolve.mli | 3 ++-
 pretyping/typing.ml     | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 26e96af48b..9522f9c249 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,7 +42,7 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-let refresh_universes dir env evd t =
+let refresh_universes ?(onlyalg=false) dir env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh dir t = 
@@ -50,7 +50,7 @@ let refresh_universes dir env evd t =
     | Sort (Type u as s) when
       (match Univ.universe_level u with
       | None -> true 
-      | Some l -> Option.is_empty (Evd.is_sort_variable evd s)) ->
+      | 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 = 
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 988938272a..6de8f5c8dc 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,7 +34,8 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : bool (* direction: true for levels lower than the existing levels *) ->
+val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) ->
+  bool (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7702355b8c..1c41a5bb3a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c =
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      Evarsolve.refresh_universes false env !evdref j.uj_type
+      Evarsolve.refresh_universes ~onlyalg:true false env !evdref j.uj_type
     else !evdref, j.uj_type
 
 let solve_evars env evdref c =
-- 
cgit v1.2.3