diff options
author | 2004-06-28 09:28:10 +0000 | |
---|---|---|
committer | 2004-06-28 09:28:10 +0000 | |
commit | a2ad1a21e99555490fb23c18e1fcec1f28502ab3 (patch) | |
tree | fd9bfba4739bccfc60615d2af937cbb0a7b8681d | |
parent | ec7ec5f6a8a0fd0cf87d9fa5381fd626cd11afad (diff) |
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
-rw-r--r-- | pretyping/detyping.ml | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 203dd4db3..40e5d4a53 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 |