Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 48 insertions, 22 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index a030284c..af54df2f 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.ml,v 1.6.2.1 2004/07/16 19:30:33 herbelin Exp $ *)
+(* $Id: decl_kinds.ml 7944 2006-01-29 16:01:32Z herbelin $ *)
+
+open Util
 
 (* Informal mathematical status of declarations *)
 
@@ -14,23 +16,32 @@ type locality_flag = (*bool (* local = true; global = false *)*)
   | Local
   | Global
 
-(* Kinds used at parsing time *)
+type boxed_flag = bool
 
 type theorem_kind =
   | Theorem
   | Lemma
   | Fact
   | Remark
+  | Property
+  | Proposition
+  | Corollary
 
 type definition_object_kind =
   | Definition
   | Coercion
   | SubClass
   | CanonicalStructure
+  | Example
+  | Fixpoint
+  | CoFixpoint
+  | Scheme
+  | StructureComponent
+  | IdentityCoercion
 
 type strength = locality_flag (* For compatibility *)
 
-type type_as_formula_kind = Definitional | Logical | Conjectural
+type assumption_object_kind = Definitional | Logical | Conjectural
 
 (* [assumption_kind] 
 
@@ -40,36 +51,51 @@ type type_as_formula_kind = Definitional | Logical | Conjectural
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality_flag * type_as_formula_kind
+type assumption_kind = locality_flag * assumption_object_kind
 
-type definition_kind = locality_flag * definition_object_kind
+type definition_kind = locality_flag * boxed_flag * definition_object_kind
 
 (* Kinds used in proofs *)
 
-type global_goal_kind =
-  | DefinitionBody
+type goal_object_kind =
+  | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind =
-  | IsGlobal of global_goal_kind
-  | IsLocal
+type goal_kind = locality_flag * goal_object_kind
 
 (* Kinds used in library *)
 
-type local_theorem_kind = LocalStatement
-
-type 'a mathematical_kind =
-  | IsAssumption of type_as_formula_kind
-  | IsDefinition
-  | IsConjecture
-  | IsProof of 'a
-
-type global_kind = theorem_kind mathematical_kind
-type local_kind = local_theorem_kind mathematical_kind
+type logical_kind =
+  | IsAssumption of assumption_object_kind
+  | IsDefinition of definition_object_kind
+  | IsProof of theorem_kind
 
 (* Utils *)
 
-let theorem_kind_of_goal_kind = function
-  | DefinitionBody -> IsDefinition
+let logical_kind_of_goal_kind = function
+  | DefinitionBody d -> IsDefinition d
   | Proof s -> IsProof s
 
+let string_of_theorem_kind = function
+  | Theorem -> "Theorem"
+  | Lemma -> "Lemma"
+  | Fact -> "Fact"
+  | Remark -> "Remark"
+  | Property -> "Property"
+  | Proposition -> "Proposition"
+  | Corollary -> "Corollary"
+
+let string_of_definition_kind (l,boxed,d) =
+  match (l,d) with
+  | Local, Coercion -> "Coercion Local"
+  | Global, Coercion -> "Coercion"
+  | Local, Definition -> "Let"
+  | Global, Definition -> if boxed then "Boxed Definition" else "Definition"
+  | Local, SubClass -> "Local SubClass"
+  | Global, SubClass -> "SubClass"
+  | Global, CanonicalStructure -> "Canonical Structure"
+  | Global, Example -> "Example"
+  | Local, (CanonicalStructure|Example) ->
+      anomaly "Unsupported local definition kind"
+  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion)
+      -> anomaly "Internal definition kind"