From 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 13 Apr 2011 14:29:02 +0000
Subject: 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
---
 library/decl_kinds.ml  | 41 +++++++++++++++++++----------------------
 library/decl_kinds.mli | 10 ++++------
 library/declare.ml     |  3 +--
 3 files changed, 24 insertions(+), 30 deletions(-)

(limited to 'library')

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 *)
 
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 1e4ad07e8..88ef763c9 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -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 *)
 
@@ -74,7 +72,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 * polymorphic * definition_object_kind -> string
+  locality * definition_object_kind -> string
 
 (** About locality *)
 
diff --git a/library/declare.ml b/library/declare.ml
index ec713d5b2..c566cedfd 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -160,8 +160,7 @@ 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_polymorphic = ce.const_entry_polymorphic;
-	 const_entry_opaque = ce.const_entry_opaque }
+         const_entry_opaque = ce.const_entry_opaque }
   | cd -> cd
 
 let declare_constant_common id dhyps (cd,kind) =
-- 
cgit v1.2.3