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/vernacentries.ml | |
| parent | 404a041fce68b4f7072de0b91b4e136f04250482 (diff) | |
Moving interpretation of user-level universes in constrintern.ml.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc03994ca6..2ca414b453 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -550,7 +550,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms = let env0 = Global.env () in let flags = Pretyping.{ all_no_fail_flags with program_mode } in let decl = fst (List.hd thms) in - let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in + let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in |