diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:29:02 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:29:02 +0000 |
| commit | 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e (patch) | |
| tree | 0eeffe9b7b098ad653ffeb6ad963c62223245d0e /library/decl_kinds.ml | |
| parent | 3b11686e4f78f6d166f84d990ac4fedb4d3e800a (diff) | |
Revert "Add [Polymorphic] flag for defs"
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719.
Conflicts:
kernel/term_typing.ml
test-suite/success/polymorphism.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/decl_kinds.ml')
| -rw-r--r-- | library/decl_kinds.ml | 41 |
1 files changed, 19 insertions, 22 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index bdc855869..ba40f98c0 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,8 +15,6 @@ type locality = | Local | Global -type polymorphic = bool - type theorem_kind = | Theorem | Lemma @@ -50,9 +48,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind +type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * polymorphic * definition_object_kind +type definition_kind = locality * definition_object_kind (* Kinds used in proofs *) @@ -60,7 +58,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind +type goal_kind = locality * goal_object_kind (* Kinds used in library *) @@ -84,23 +82,22 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind (gl,p,k) = - let s = match gl, k with - | Local, Coercion -> "Coercion Local" - | Global, Coercion -> "Coercion" - | Local, Definition -> "Let" - | Global, Definition -> "Definition" - | Local, SubClass -> "Local SubClass" - | Global, SubClass -> "SubClass" - | Global, CanonicalStructure -> "Canonical Structure" - | Global, Example -> "Example" - | Local, (CanonicalStructure|Example) -> - anomaly "Unsupported local definition kind" - | Local, Instance -> "Instance" - | Global, Instance -> "Global Instance" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) - -> anomaly "Internal definition kind" - in if p then "Polymorphic " ^ s else s +let string_of_definition_kind def = + match def with + | Local, Coercion -> "Coercion Local" + | Global, Coercion -> "Coercion" + | Local, Definition -> "Let" + | Global, Definition -> "Definition" + | Local, SubClass -> "Local SubClass" + | Global, SubClass -> "SubClass" + | Global, CanonicalStructure -> "Canonical Structure" + | Global, Example -> "Example" + | Local, (CanonicalStructure|Example) -> + anomaly "Unsupported local definition kind" + | Local, Instance -> "Instance" + | Global, Instance -> "Global Instance" + | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) + -> anomaly "Internal definition kind" (* Strength *) |