diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-02 15:50:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-17 16:29:07 +0200 |
| commit | dbc820f0df53218e730eba34b44a3b1901f13b9e (patch) | |
| tree | 11720b5f35bbc51202eec80e27eca14e32f8064c /vernac/record.ml | |
| parent | 3e7863e9369d38537685576a8642dbe0c062d0c5 (diff) | |
Deprecate mixing univ minimization and evm normalization functions.
Normalization sounds like it should be semantically noop.
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 78e68e8a3..b89c0060d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -168,7 +168,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in - let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let sigma = Evd.minimize_universes sigma in let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in let typ = EConstr.to_constr sigma typ in |