From e6cbfce752d7b7bce9dfa8635501342f29e9a18f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 11 Jul 2004 18:46:38 +0000
Subject: Backtrack sur l'eta-expansion systematique et incorrect du predicat
 du Cases (c'est au moment de la construction dans Indrec qu'il faut
 eta-expanser -cf bug #784)

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

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 40e5d4a536..db4264195d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -246,16 +246,7 @@ let detype_case computable detype detype_eqn testdep
             let nl,typ = decompose_lam k p in
 	    let n,typ = match typ with 
               | RLambda (_,x,t,c) -> x, c
-	      | _ -> 
-		  let id = match tomatch with
-		    | RVar (_,id) -> id
-		    | _ -> id_of_string "x" in
-                  let x = next_ident_away id avoid in
-		  let a = RVar (dummy_loc,x) in
-		  let typ = match typ with
-                    | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                    | _ -> (RApp (dummy_loc,typ,[a])) in
-		  Name x, typ in
+	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
 	      else 
-- 
cgit v1.2.3