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.
---
 plugins/cc/cctac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index ba34d49bb0..c8d857b31f 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 =
-- 
cgit v1.2.3