aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/declare.ml52
-rw-r--r--interp/discharge.ml6
-rw-r--r--interp/modintern.ml4
3 files changed, 30 insertions, 32 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 7a32018c0e..1e972d3e35 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 *)
@@ -358,27 +358,26 @@ let inInductive : mutual_inductive_entry -> obj =
let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
let id = Label.to_id label in
- let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
- Recordops.declare_primitive_projection p;
- (* ^ needs to happen before declaring the constant, otherwise
- Heads gets confused. *)
let univs = match univs with
| 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
let entry = definition_entry ~types ~univs term in
- ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent))
+ let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+ let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+ Recordops.declare_primitive_projection p cst
+
let declare_projections univs mind =
let env = Global.env () in
@@ -473,36 +472,33 @@ type universe_source =
type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
let check_exists sp =
- let depth = sections_depth () in
- let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
if Nametab.exists_universe sp then
alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
else ()
-let qualify_univ i sp src id =
- let open Libnames in
+let qualify_univ i dp src id =
match src with
| BoundUniv | UnqualifiedUniv ->
- let sp = dirpath sp in
- i, make_path sp id
+ i, Libnames.make_path dp id
| QualifiedUniv l ->
- let sp = dirpath sp in
- let sp = DirPath.repr sp in
- Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id
+ let dp = DirPath.repr dp in
+ Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
-let do_univ_name ~check i sp src (id,univ) =
- let i, sp = qualify_univ i sp src id in
+let do_univ_name ~check i dp src (id,univ) =
+ let i, sp = qualify_univ i dp src id in
if check then check_exists sp;
Nametab.push_universe i sp univ
let cache_univ_names ((sp, _), (src, univs)) =
- List.iter (do_univ_name ~check:true (Nametab.Until 1) sp src) univs
+ let depth = sections_depth () in
+ let dp = pop_dirpath_n depth (dirpath sp) in
+ List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
let load_univ_names i ((sp, _), (src, univs)) =
- List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs
+ List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs
let open_univ_names i ((sp, _), (src, univs)) =
- List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs
+ List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs
let discharge_univ_names = function
| _, (BoundUniv, _) -> None
@@ -520,12 +516,12 @@ 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
| IndRef (c, _) -> Label.to_id @@ MutInd.label c
- | VarRef id -> id
+ | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
| ConstructRef _ ->
anomaly ~label:"declare_univ_binders"
Pp.(str "declare_univ_binders on an constructor reference")
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 21b2e85e8f..eeda5a6867 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -79,13 +79,15 @@ let process_inductive info modlist mib =
| Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
| Polymorphic_ind auctx ->
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let nas = Univ.AUContext.names auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Polymorphic_ind_entry auctx
+ subst, Polymorphic_ind_entry (nas, auctx)
| Cumulative_ind cumi ->
let auctx = Univ.ACumulativityInfo.univ_context cumi in
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+ let nas = Univ.AUContext.names auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
+ subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx)
in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
let inds =
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 51e27299e3..60056dfd90 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,8 +107,8 @@ let transl_with_decl env base kind = function
let c, ectx = interp_constr env sigma c in
let poly = lookup_polymorphism env base kind fqid in
begin match UState.check_univ_decl ~poly ectx udecl with
- | Entries.Polymorphic_const_entry ctx ->
- let inst, ctx = Univ.abstract_universes ctx in
+ | Entries.Polymorphic_const_entry (nas, ctx) ->
+ let inst, ctx = Univ.abstract_universes nas ctx in
let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
let c = EConstr.to_constr sigma c in
WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:34:00 +0000