diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 20:21:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:34:58 +0200 |
| commit | fa1782e05eeb6f18871d26cc43670d35ed73bf23 (patch) | |
| tree | a182392b3f511f6a2f8f8899239802cf3d310532 /tactics | |
| parent | 66e52c88076ba830c8c8b3cf8e4bb77959fb7843 (diff) | |
[dumpglob] Move dumpglob-specific data to dumpglob.
The whole business of cst_kind is fishy tho, it seems to me that it
should be removed from the libobject path.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index b994585e8a..6a7f728abc 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -53,7 +53,7 @@ let load_constant i ((sp,kn), obj) = alreadydeclared (Id.print (basename sp) ++ str " already exists"); let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (ConstRef con); - Decls.add_constant_kind con obj.cst_kind + Dumpglob.add_constant_kind con obj.cst_kind let cooking_info segment = let modlist = replacement_context () in @@ -94,7 +94,7 @@ let cache_constant ((sp,kn), obj) = Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - Decls.add_constant_kind (Constant.make1 kn) obj.cst_kind + Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in |