From 094b40758cb4278b33a87e5633cf4ac716f348b4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Dec 2002 11:49:08 +0000
Subject: Affinement affichage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3473 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4c6d24833b..86bca87ebc 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -260,14 +260,15 @@ let rec detype tenv avoid env t =
 	if tag = RegularStyle then
 	  RCases (dummy_loc,pred,[tomatch],eqnl)
 	else
-	  let bl = Array.map (detype tenv avoid env) bl in
 	  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
+	      | RLetIn (loc,na,b,c) ->
+		  RLetIn (loc,na,b,remove_type (n-1) c)
+	      | c -> c in
+	  let bl = Array.map (detype tenv avoid env) bl in
 	  let bl = array_map2 remove_type consnargsl bl in
 	  ROrderedCase (dummy_loc,tag,pred,tomatch,bl)
 	
-- 
cgit v1.2.3