From a002d6ef127b4f0103012c23fc5d272739649043 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 20 Apr 2000 15:51:40 +0000
Subject: Abstraction du type typed_type (un pas vers les jugements 2 niveaux)

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

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 539a953a1..241e4ec05 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -22,7 +22,7 @@ let tjudge_of_cast_safe sigma env var =
   match under_casts (fun _ -> nf_ise1) env sigma var with
     | DOP2 (Cast, b, t) ->
 	(match whd_betadeltaiota env sigma t with
-	   | DOP0 (Sort s) -> {body=b; typ=s}
+	   | DOP0 (Sort s) -> make_typed b s
 	   | _ -> anomaly "Not a type (tjudge_of_cast)")
     | c -> execute_rec_type env sigma c
 (* FIN TMP ***** *)
-- 
cgit v1.2.3