congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.

6 files changed, 19 insertions, 26 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 117bc4e5f..2cc57c38c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -754,7 +754,7 @@ let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
 exception AlreadyDeclared
-	    
+
 let add_universe vlev strict g =
   try
     let _arcv = UMap.find vlev g in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index ba34d49bb..c8d857b31 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -262,7 +262,7 @@ let assert_before n c =
   end
 
 let refresh_type env evm ty =
-  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~propset:true
+  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
 			      (Some false) env evm ty
 
 let refresh_universes ty k =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c2d47790d..0db309f94 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'
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 9ee815ebc..f94c83b6d 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 *) ->
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index a70d91963..0b0e93eb5 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -131,3 +131,17 @@ End bug_2447.
 
 
 
+(* Example by Jonathan Leivant, congruence up to universes *)
+Section JLeivant.
+  Variables S1 S2 : Set.
+
+  Definition T1 : Type := S1.
+  Definition T2 : Type := S2.
+
+  Goal T1 = T1.
+    congruence.
+    Undo.
+    unfold T1.
+    congruence.
+  Qed.
+End JLeivant.
diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v
deleted file mode 100644
index 873d2f9f7..000000000
--- a/test-suite/success/congruence.v
+++ /dev/null
@@ -1,21 +0,0 @@
-(* Example by Jonathan Leivant, congruence and tauto up to universes *)
-Variables S1 S2 : Set.
-
-Goal @eq Type S1 S2 -> @eq Type S1 S2.
-intro H.
-tauto.
-Qed.
-
-Definition T1 : Type := S1.
-Definition T2 : Type := S2.
-
-Goal T1 = T1.
-congruence.
-Undo.
-tauto.
-Undo.
-unfold T1.
-congruence.
-Undo.
-tauto.
-Qed.