From dfe97724fb6034fc06b3ef693f6a3ed94733adbc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Oct 2006 20:11:08 +0000
Subject: Compatibilité du polymorphisme de constantes avec les sections.
 Amélioration affichage des univers. Réparation de petits oublis du premier
 commit. Essai d'une nouvelle stratégie : si le type d'une constante est
 mentionné explicitement, la constante est monomorphe dans Type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cooking.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 68d301eb46..e6d7613b00 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -16,6 +16,7 @@ open Sign
 open Declarations
 open Environ
 open Reduction
+open Term_typing
 
 (*s Cooking the constants. *)
 
@@ -129,7 +130,6 @@ let cook_constant env r =
     | PolymorphicArity (ctx,s) ->
 	let t = mkArity (ctx,Type s.poly_level) in
 	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
-	let ctx,_ = dest_prod env typ in
-	PolymorphicArity (ctx,s) in
+	Typeops.make_polymorphic_if_arity env typ in
   let boxed = Cemitcodes.is_boxed cb.const_body_code in
   (body, typ, cb.const_constraints, cb.const_opaque, boxed)
-- 
cgit v1.2.3