diff options
| author | herbelin | 2004-06-27 19:06:36 +0000 |
|---|---|---|
| committer | herbelin | 2004-06-27 19:06:36 +0000 |
| commit | 008253465b65c0c50477bf830bab3590564706a4 (patch) | |
| tree | 3e247f3c4d02f7f0c6b4bff32157076a627c3b5d | |
| parent | 9763ba62c1a8adf56d179fd541349414237fe09b (diff) | |
Correction affichage v8 des records avec let (bug #798)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5830 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/detyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 9666008c39..203dd4db3e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -277,10 +277,10 @@ let detype_case computable detype detype_eqn testdep let rec decomp_lam_force n avoid l p = if n = 0 then (List.rev l,p) else match p with - | RLambda (_,(Name id as na),_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,c) -> - decomp_lam_force (n-1) avoid (na::l) c + | RLambda (_,na,_,c) -> + decomp_lam_force (n-1) (name_cons na avoid) (na::l) c + | RLetIn (_,na,_,c) -> + decomp_lam_force (n-1) (name_cons na avoid) (na::l) c | _ -> let x = Nameops.next_ident_away (id_of_string "x") avoid in decomp_lam_force (n-1) (x::avoid) (Name x :: l) |