diff options
| author | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
| commit | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (patch) | |
| tree | 754bd11791e63df535dff44a58e126ff9330b8ea /interp/declare.ml | |
| parent | 5d90e05b35f85607c43888b9adb0319e98a81fb4 (diff) | |
| parent | 8272c4e08f3c045a27d0bcb89a67a167625bf233 (diff) | |
Merge PR #8601: Move bound universe names to abstract contexts
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 7a32018c0e..fe8fc7c969 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -219,7 +219,7 @@ let cache_variable ((sp,_),o) = let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with | Monomorphic_const_entry uctx -> false, uctx - | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx + | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in (** We must declare the universe constraints before type-checking the @@ -339,7 +339,7 @@ let infer_inductive_subtyping mind_ent = match mind_ent.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> mind_ent - | Cumulative_ind_entry cumi -> + | Cumulative_ind_entry (_, cumi) -> begin let env = Global.env () in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) @@ -366,14 +366,14 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter | Monomorphic_ind_entry _ -> (** Global constraints already defined through the inductive *) Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry ctx -> - Polymorphic_const_entry ctx - | Cumulative_ind_entry ctx -> - Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + | Polymorphic_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, ctx) + | Cumulative_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx) in let term, types = match univs with | Monomorphic_const_entry _ -> term, types - | Polymorphic_const_entry ctx -> + | Polymorphic_const_entry (_, ctx) -> let u = Univ.UContext.instance ctx in Vars.subst_instance_constr u term, Vars.subst_instance_constr u types in @@ -520,7 +520,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - UnivNames.register_universe_binders gr pl + () else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c |