diff options
| author | Maxime Dénès | 2018-09-25 14:33:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-05 08:57:56 +0200 |
| commit | 650c65af484c45f4e480252b55d148bcc198be6c (patch) | |
| tree | ebc0a8e7777ddd90515abcdea2e8975d1d968640 /interp/declare.ml | |
| parent | 3f2a6d8e99f31bbd9383119cac39ed0bcaabc37d (diff) | |
[kernel] Remove section paths from `KerName.t`
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 23c68b5e18..f4e57073cc 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -78,7 +78,6 @@ let check_exists sp = let cache_constant ((sp,kn), obj) = let id = basename sp in - let _,dir,_ = KerName.repr kn in let kn' = match obj.cst_decl with | None -> @@ -87,7 +86,7 @@ let cache_constant ((sp,kn), obj) = else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") | Some decl -> let () = check_exists sp in - Global.add_constant dir id decl + Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl in assert (Constant.equal kn' (Constant.make1 kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); @@ -136,7 +135,7 @@ let register_side_effect (c, role) = cst_kind = IsProof Theorem; cst_locl = false; } in - let id = Label.to_id (pi3 (Constant.repr3 c)) in + let id = Label.to_id (Constant.label c) in ignore(add_leaf id o); update_tables c; match role with @@ -311,8 +310,7 @@ let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter check_exists (List.map fst names); let id = basename sp in - let _,dir,_ = KerName.repr kn in - let kn' = Global.add_mind dir id mie in + let kn' = Global.add_mind id mie in assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; |