Extension du polymorphisme de sorte au cas des définitions dans Type.

(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 1 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 264bd6215..9cfce4303 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -119,6 +119,12 @@ type global_declaration =
   | ConstantEntry of constant_entry
   | GlobalRecipe of Cooking.recipe
 
+let hcons_constant_type = function
+  | NonPolymorphicType t ->
+      NonPolymorphicType (hcons1_constr t)
+  | PolymorphicArity (ctx,s) ->
+      PolymorphicArity (map_rel_context hcons1_constr ctx,s)
+
 let hcons_constant_body cb =
   let body = match cb.const_body with
       None -> None
@@ -127,7 +133,7 @@ let hcons_constant_body cb =
   in
     { cb with
 	const_body = body;
-	const_type = hcons1_constr cb.const_type }
+	const_type = hcons_constant_type cb.const_type }
 
 let add_constant dir l decl senv =
   check_label l senv.labset;