From 9ee4a02e9234ad6cebb3365881250d7539d00d03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Dec 2015 15:14:23 +0100
Subject: Fix in setoid_rewrite in Type: avoid the generation of a rigid
 universe on applications of inverse (flip) on a crelation.

This was poluting universe constraints of lemmas using generalized
rewriting in Type.
---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 182c232ae9..a230ea251a 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -403,7 +403,7 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let evd, (sort,_) = Evarutil.new_type_evar env evd Evd.univ_flexible in
+    let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
-- 
cgit v1.2.3