diff options
| -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 |