aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-13 14:26:59 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-13 14:26:59 +0000
commitd98dfbcae463f8d699765e2d7004becd7714d6cf (patch)
tree976e3e3ae284485cabd567d7c3504bc7b8817554 /library
parent5113afbb6e8c1f9122b37c37b0561c529c406256 (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')
-rw-r--r--library/decl_kinds.ml41
-rw-r--r--library/decl_kinds.mli10
-rw-r--r--library/declare.ml3
3 files changed, 30 insertions, 24 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 *)
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 88ef763c9..1e4ad07e8 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -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 *)
@@ -72,7 +74,7 @@ type logical_kind =
val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
val string_of_theorem_kind : theorem_kind -> string
val string_of_definition_kind :
- locality * definition_object_kind -> string
+ locality * polymorphic * definition_object_kind -> string
(** About locality *)
diff --git a/library/declare.ml b/library/declare.ml
index c566cedfd..ec713d5b2 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -160,7 +160,8 @@ let hcons_constant_declaration = function
DefinitionEntry
{ const_entry_body = hcons1_constr ce.const_entry_body;
const_entry_type = Option.map hcons1_constr ce.const_entry_type;
- const_entry_opaque = ce.const_entry_opaque }
+ const_entry_polymorphic = ce.const_entry_polymorphic;
+ const_entry_opaque = ce.const_entry_opaque }
| cd -> cd
let declare_constant_common id dhyps (cd,kind) =