diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-23 19:05:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-23 19:05:52 +0000 |
| commit | d134b5afaf26a67149d999e95bd21b264b61429b (patch) | |
| tree | ffefef4b65a1fc4ad5c1656e8acebd65091f17f2 /library/decl_kinds.ml | |
| parent | 25c26b44bd27c2d94e4751a0722fa1ea1e7b242f (diff) | |
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
Diffstat (limited to 'library/decl_kinds.ml')
| -rw-r--r-- | library/decl_kinds.ml | 27 |
1 files changed, 12 insertions, 15 deletions
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 *) |