From a2ad1a21e99555490fb23c18e1fcec1f28502ab3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Jun 2004 09:28:10 +0000
Subject: Double bug d'affichage des cases dépendants (bug #784)

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

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 203dd4db3e..40e5d4a536 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -231,11 +231,11 @@ let detype_case computable detype detype_eqn testdep
         | Some p ->
             let decompose_lam k c =
               let rec lamdec_rec l avoid k c =
-                if k = 0 then l,c else match c with
+                if k = 0 then List.rev l,c else match c with
                   | RLambda (_,x,t,c) -> 
                       lamdec_rec (x::l) (name_cons x avoid) (k-1) c
                   | c -> 
-                      let x = next_ident_away (id_of_string "xx") avoid in
+                      let x = next_ident_away (id_of_string "x") avoid in
                       lamdec_rec ((Name x)::l) (x::avoid) (k-1)
                         (let a = RVar (dummy_loc,x) in
                           match c with
@@ -246,7 +246,16 @@ 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
-	      | _ -> Anonymous, typ in
+	      | _ -> 
+		  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
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
 	      else 
-- 
cgit v1.2.3