From 359e4ffe307d7d8dd250735373fc6354a58ecff5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Oct 2006 19:35:09 +0000
Subject: 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
---
 contrib/xml/doubleTypeInference.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/xml/doubleTypeInference.ml')

diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index a3336817e0..c7d3b4ff0c 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -122,7 +122,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         Typeops.judge_of_variable env id
 	  
      | T.Const c ->
-        E.make_judge cstr (E.constant_type env c)
+        E.make_judge cstr (Typeops.type_of_constant env c)
 	  
      | T.Ind ind ->
         E.make_judge cstr (Inductiveops.type_of_inductive env ind)
-- 
cgit v1.2.3