From bf578ad5e2f63b7a36aeaef5e0597101db1bd24a Mon Sep 17 00:00:00 2001
From: gregoire
Date: Fri, 2 Dec 2005 10:01:15 +0000
Subject: Changement des named_context Ajout de cast indiquant au kernel la
 strategie a suivre Resolution du bug sur les coinductifs

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

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b62e7b007a..f76c5ffe33 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -19,8 +19,6 @@ open Inductive
 open Environ
 open Entries
 open Type_errors
-open Cemitcodes
-open Cbytegen
 open Indtypes
 open Typeops
 
@@ -28,13 +26,10 @@ let constrain_type env j cst1 = function
   | None -> j.uj_type, cst1
   | Some t -> 
       let (tj,cst2) = infer_type env t in
-      let cst3 =
-	try vm_conv_leq env j.uj_type tj.utj_val
-	with NotConvertible -> error_actual_type env j tj.utj_val in
+      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
       assert (t = tj.utj_val);
       t, Constraint.union (Constraint.union cst1 cst2) cst3
 
-
 let translate_local_def env (b,topt) =
   let (j,cst) = infer env b in
   let (typ,cst) = constrain_type env j cst topt in
@@ -99,7 +94,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) =
 	  (global_vars_set env (Declarations.force b)) 
 	  (global_vars_set env typ)
   in
-  let tps = from_val (compile_constant_body env body op boxed) in
+  let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
   let hyps = keep_hyps env ids in
     { const_hyps = hyps;
       const_body = body;
-- 
cgit v1.2.3