From a5b631f7260e7d29defd8bd5c67db543742c9ecd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 17:40:04 +0200
Subject: congruence/univs: properly refresh (fix #4609)

In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
---
 pretyping/evarsolve.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarsolve.mli')

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 918ba12f0f..9ee815ebc0 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,8 +34,12 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : ?status:Evd.rigid ->
-			?onlyalg:bool (* Only algebraic universes *) ->
+val refresh_universes :
+  ?status:Evd.rigid ->
+  ?onlyalg:bool (* Only algebraic universes *) ->
+  ?propset:bool ->
+  (* Also refresh Prop and Set universes, so that the returned type can be any supertype
+     of the original type *)
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
-- 
cgit v1.2.3


From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 18:31:01 +0200
Subject: congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
---
 pretyping/evarsolve.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/evarsolve.mli')

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 9ee815ebc0..f94c83b6dc 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -37,7 +37,7 @@ val evar_define : conv_fun -> ?choose:bool -> env -> evar_map ->
 val refresh_universes :
   ?status:Evd.rigid ->
   ?onlyalg:bool (* Only algebraic universes *) ->
-  ?propset:bool ->
+  ?refreshset:bool ->
   (* Also refresh Prop and Set universes, so that the returned type can be any supertype
      of the original type *)
   bool option (* direction: true for levels lower than the existing levels *) ->
-- 
cgit v1.2.3