diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:26:59 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:26:59 +0000 |
| commit | d98dfbcae463f8d699765e2d7004becd7714d6cf (patch) | |
| tree | 976e3e3ae284485cabd567d7c3504bc7b8817554 /library/decl_kinds.ml | |
| parent | 5113afbb6e8c1f9122b37c37b0561c529c406256 (diff) | |
Add [Polymorphic] flag for defs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/decl_kinds.ml')
| -rw-r--r-- | library/decl_kinds.ml | 41 |
1 files changed, 22 insertions, 19 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index ba40f98c0..bdc855869 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,6 +15,8 @@ type locality = | Local | Global +type polymorphic = bool + type theorem_kind = | Theorem | Lemma @@ -48,9 +50,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * assumption_object_kind +type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * definition_object_kind +type definition_kind = locality * polymorphic * definition_object_kind (* Kinds used in proofs *) @@ -58,7 +60,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * goal_object_kind +type goal_kind = locality * polymorphic * goal_object_kind (* Kinds used in library *) @@ -82,22 +84,23 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -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" +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 (* Strength *) |