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.
---
 plugins/setoid_ring/newring.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 33798c43c8..3d6bfda0b2 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -29,7 +29,6 @@ open Tacinterp
 open Libobject
 open Printer
 open Declare
-open Decl_kinds
 open Entries
 open Newring_ast
 open Proofview.Notations
@@ -158,7 +157,7 @@ let decl_constant na univs c =
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
-	     IsProof Lemma))
+             Decls.(IsProof Lemma)))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-- 
cgit v1.2.3