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 ++++++++++++++++++++++-------------------
 1 file changed, 22 insertions(+), 19 deletions(-)

(limited to 'library/decl_kinds.ml')

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