diff options
| author | Matthieu Sozeau | 2015-12-04 15:14:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-12-04 15:14:23 +0100 |
| commit | 9ee4a02e9234ad6cebb3365881250d7539d00d03 (patch) | |
| tree | fc917c980e80944343d81851a9666117c35d15fa /tactics | |
| parent | f41968d8c240db4653d0b9fe76e1646cd7c6fb68 (diff) | |
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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |