From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 library/decl_kinds.ml | 29 +++++++++++++++++++++--------
 1 file changed, 21 insertions(+), 8 deletions(-)

(limited to 'library/decl_kinds.ml')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index af54df2f..8f2525b8 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.ml 7944 2006-01-29 16:01:32Z herbelin $ *)
+(* $Id: decl_kinds.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
 
 open Util
+open Libnames
 
 (* Informal mathematical status of declarations *)
 
-type locality_flag = (*bool (* local = true; global = false *)*)
+type locality =
   | Local
   | Global
 
@@ -38,8 +39,8 @@ type definition_object_kind =
   | Scheme
   | StructureComponent
   | IdentityCoercion
-
-type strength = locality_flag (* For compatibility *)
+  | Instance
+  | Method
 
 type assumption_object_kind = Definitional | Logical | Conjectural
 
@@ -51,9 +52,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality_flag * assumption_object_kind
+type assumption_kind = locality * assumption_object_kind
 
-type definition_kind = locality_flag * boxed_flag * definition_object_kind
+type definition_kind = locality * boxed_flag * definition_object_kind
 
 (* Kinds used in proofs *)
 
@@ -61,7 +62,7 @@ type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality_flag * goal_object_kind
+type goal_kind = locality * goal_object_kind
 
 (* Kinds used in library *)
 
@@ -97,5 +98,17 @@ let string_of_definition_kind (l,boxed,d) =
   | Global, Example -> "Example"
   | Local, (CanonicalStructure|Example) ->
       anomaly "Unsupported local definition kind"
-  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion)
+  | Local, Instance -> "Instance"
+  | Global, Instance -> "Global Instance"
+  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method)
       -> anomaly "Internal definition kind"
+
+(* Strength *)
+
+let strength_of_global = function
+  | VarRef _ -> Local
+  | IndRef _ | ConstructRef _ | ConstRef _ -> Global
+
+let string_of_strength = function
+  | Local -> "Local"
+  | Global -> "Global"
-- 
cgit v1.2.3