From d134b5afaf26a67149d999e95bd21b264b61429b Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 23 Oct 2003 19:05:52 +0000
Subject: Conjecture declare maintenant un axiome; reorganisation
 VernacDefinition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/decl_kinds.ml | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

(limited to 'library/decl_kinds.ml')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index a47fb9086..74e256684 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -10,6 +10,10 @@
 
 (* Informal mathematical status of declarations *)
 
+type locality_flag = (*bool (* local = true; global = false *)*)
+  | Local
+  | Global
+
 (* Kinds used at parsing time *)
 
 type theorem_kind =
@@ -17,24 +21,16 @@ type theorem_kind =
   | Lemma
   | Fact
   | Remark
-  | Conjecture
 
-type definitionkind =
-  | LDefinition
-  | GDefinition
-  | LCoercion
-  | GCoercion
-  | LSubClass
-  | GSubClass
-  | SCanonical
-
-type locality_flag = (*bool (* local = true; global = false *)*)
-  | Local
-  | Global
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
 
 type strength = locality_flag (* For compatibility *)
 
-type type_as_formula_kind = Definitional | Logical
+type type_as_formula_kind = Definitional | Logical | Conjectural
 
 (* [assumption_kind] 
 
@@ -42,10 +38,11 @@ type type_as_formula_kind = Definitional | Logical
    ------------------------------------
    Definitional |  Variable   | Parameter
    Logical      |  Hypothesis | Axiom
+
 *)
 type assumption_kind = locality_flag * type_as_formula_kind
 
-type definition_kind = locality_flag
+type definition_kind = locality_flag * definition_object_kind
 
 (* Kinds used in proofs *)
 
-- 
cgit v1.2.3