diff options
| author | Pierre-Marie Pédrot | 2018-09-28 15:32:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-28 15:32:04 +0200 |
| commit | f070a1f6eb99de1461d5a846a4f9ed47dafa79c6 (patch) | |
| tree | a8b2ac7b57539abfe3dffe4184cca3970301864a /interp | |
| parent | a0bdf071f8767aab18b24f19321041e18263d574 (diff) | |
| parent | 2566d45fcc05c1cd80ba2ac16ef342e7f145f01a (diff) | |
Merge PR #8479: Fix #8478: Undeclared universe anomaly with sections
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 22e6cf9d1c..23c68b5e18 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -491,7 +491,6 @@ let add_universe src (dp, i) = Option.iter (fun poly -> let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in Global.push_context_set poly ctx; - UnivNames.add_global_universe level poly; if poly then Lib.add_section_context ctx) optpoly @@ -580,7 +579,7 @@ let do_constraint poly l = let open Univ in let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - UnivNames.is_polymorphic level, level + Lib.is_polymorphic_univ level, level in let in_section = Lib.sections_are_opened () in let () = |