From 0f532fe6403342f2f7b0a2da07bbf4112f7f85b4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Dec 2002 08:40:25 +0000
Subject: Problèmes et améliorations divers affichage

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

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 53c9453d0b..2758dcff48 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -259,7 +259,15 @@ let rec detype tenv avoid env t =
 	  RCases (dummy_loc,pred,[tomatch],eqnl)
 	else
 	  let bl = Array.map (detype tenv avoid env) bl in
-	  ROrderedCase (dummy_loc,LetStyle,pred,tomatch,bl)
+	  let rec remove_type n c = if n = 0 then c else
+	    match c with
+	      | RLambda (loc,na,t,c) ->
+		  let h = RHole (loc,AbstractionType na) in
+		  RLambda (loc,na,h,remove_type (n-1) c)
+	      | RLetIn (loc,na,b,c) -> RLetIn (loc,na,b,remove_type (n-1) c)
+	      | _ -> anomaly "Not a context" in
+	  let bl = array_map2 remove_type consnargsl bl in
+	  ROrderedCase (dummy_loc,tag,pred,tomatch,bl)
 	
     | Fix (nvn,recdef) -> detype_fix tenv avoid env (RFix nvn) recdef
     | CoFix (n,recdef) -> detype_fix tenv avoid env (RCoFix n) recdef
-- 
cgit v1.2.3