From d98dfbcae463f8d699765e2d7004becd7714d6cf Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 13 Apr 2011 14:26:59 +0000
Subject: Add [Polymorphic] flag for defs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/decl_kinds.ml  | 41 ++++++++++++++++++++++-------------------
 library/decl_kinds.mli | 10 ++++++----
 library/declare.ml     |  3 ++-
 3 files changed, 30 insertions(+), 24 deletions(-)

(limited to 'library')

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) =
-- 
cgit v1.2.3