diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 36 |
1 files changed, 16 insertions, 20 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index fe8fc7c969..1e972d3e35 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -358,10 +358,6 @@ 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 *) @@ -378,7 +374,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter 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 @@ -525,7 +521,7 @@ let declare_univ_binders gr pl = 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") |