From 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e Mon Sep 17 00:00:00 2001 From: msozeau 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 --- kernel/entries.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel/entries.ml') diff --git a/kernel/entries.ml b/kernel/entries.ml index 32dfaae8f..28f11c9af 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -55,10 +55,9 @@ type mutual_inductive_entry = { (*s Constants (Definition/Axiom) *) type definition_entry = { - const_entry_body : constr; - const_entry_type : types option; - const_entry_polymorphic : bool; - const_entry_opaque : bool } + const_entry_body : constr; + const_entry_type : types option; + const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) -- cgit v1.2.3