From ab44b04dfc706a66de6ce5c6ad3df1ece6920918 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 13 Oct 2000 16:14:49 +0000
Subject: Suppression d'un test inutile dans RCast

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@707 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 93a03dcfa1..a7ac436b60 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -374,7 +374,11 @@ match cstr with   (* O
   let tj = pretype_type (valcon_of_tycon tycon) env isevars lvar lmeta t in
   let tj = type_judgment env !isevars tj in
   let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in
-  inh_conv_coerce_to loc env isevars cj (assumption_of_type_judgment tj)
+  match tycon with
+    | None  -> cj
+    | Some t' -> 
+	let tj' = Retyping.get_assumption_of env !isevars t' in
+	inh_conv_coerce_to loc env isevars cj tj'
 
 and pretype_type valcon env isevars lvar lmeta = function
 | RHole loc ->
-- 
cgit v1.2.3