From 66e52c88076ba830c8c8b3cf8e4bb77959fb7843 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 20:14:46 +0200
Subject: [api] Refactor most of `Decl_kinds`

We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.

The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.

Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.

IMO this needs more work, but this should be a good start.
---
 vernac/declareDef.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index d229973936..7487c99f56 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Decl_kinds
 open Declare
 open Globnames
 open Impargs
@@ -49,10 +48,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
   let gr = match scope with
   | Discharge ->
-      let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in
+      let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, Decls.IsDefinition kind) in
       VarRef name
   | Global local ->
-      let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in
+      let kn = declare_constant name ~local (DefinitionEntry ce, Decls.IsDefinition kind) in
       let gr = ConstRef kn in
       let () = Declare.declare_univ_binders gr udecl in
       gr
-- 
cgit v1.2.3