diff options
| author | Pierre-Marie Pédrot | 2015-12-08 18:12:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-08 18:12:27 +0100 |
| commit | e70165079e8defe490a568ece20a7029e4c1626e (patch) | |
| tree | 7e8ad97cbe6e06251fae9cc2da48acc8ab36d303 /tactics/rewrite.ml | |
| parent | 071a458681254716a83b1802d5b6a30edda37892 (diff) | |
| parent | 19ea51a4b7f7debbe5bdeb2b2689cddadd9876f4 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tactics/rewrite.ml')
| -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 9a19d4bda7..2dfebc9a3c 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -407,7 +407,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 |