diff options
| author | Pierre-Marie Pédrot | 2019-07-29 10:48:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | 58a9de2acacb05291d87fe2b656728ae05d59df4 (patch) | |
| tree | 6472556f7796bf6b8364b61ddcadd942ae6f2763 /tactics | |
| parent | 6176c2879dd989029a83642caec7cd66a2a4f527 (diff) | |
Move the Lib section data into the kernel.
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 2f9da373aa..208b8e28a7 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -63,7 +63,7 @@ let declare_universe_context ~poly ctx = let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in let uctx = Univ.ContextSet.to_context (univs, cstr) in let nas = name_instance (Univ.UContext.instance uctx) in - (Global.push_context_set true ctx; Lib.add_section_context (nas, uctx)) + Global.push_section_context (nas, uctx) else Lib.add_anonymous_leaf (input_universe_context ctx) @@ -139,8 +139,6 @@ let cache_constant ((sp,kn), obj) = in assert (Constant.equal kn' (Constant.make1 kn)); Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn)); - let cst = Global.lookup_constant kn' in - add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind let discharge_constant ((sp, kn), obj) = @@ -373,7 +371,6 @@ let declare_variable ~name ~kind d = poly in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); - add_section_variable ~name ~poly; Decls.(add_variable_data name {opaque;kind}); add_anonymous_leaf (inVariable ()); Impargs.declare_var_implicits ~impl name; @@ -422,8 +419,6 @@ let cache_inductive ((sp,kn),mie) = let id = Libnames.basename sp 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 ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names let discharge_inductive ((sp,kn),mie) = |