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.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 29af199a1e..c2d47790d5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -47,7 +47,8 @@ let refresh_level evd s =
   | None -> true
   | Some l -> not (Evd.is_flexible_level evd l)
 
-let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false)
+		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh status dir t = 
@@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
       else set_leq_sort env !evdref s s'
     in
       modified := true; evdref := evd; mkSort s'
+    | Sort (Prop _ as s) when propset && 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'
     | Prod (na,u,v) -> 
       mkProd (na,u,refresh status dir v)
     | _ -> t
-- 
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.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c2d47790d5..0db309f948 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 ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false)
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
@@ -63,7 +63,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false)
       else set_leq_sort env !evdref s s'
     in
       modified := true; evdref := evd; mkSort s'
-    | Sort (Prop _ as s) when propset && not dir ->
+    | 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'
-- 
cgit v1.2.3