diff options
| author | Hugo Herbelin | 2020-10-31 14:06:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 16:56:49 +0100 |
| commit | 78e600ac5f8aa9609cac4347c7a694428ae9d7cc (patch) | |
| tree | 54ddd0faba729e23d3cfc06c8d6457bb420a2d72 /vernac/record.ml | |
| parent | 404a041fce68b4f7072de0b91b4e136f04250482 (diff) | |
Moving interpretation of user-level universes in constrintern.ml.
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 acc97f61c1..2c56604d8f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields def poly pl ps records = let is_template = List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in - let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in + let sigma, decl = interp_univ_decl_opt env0 pl in let () = let error bk {CAst.loc; v=name} = match bk, name with |