diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2013-11-25 14:14:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2013-11-25 14:28:06 +0100 |
| commit | 32c900252a07ea7d2dd9fe15feb21ef98aee3df7 (patch) | |
| tree | f0ded05c6d99135fa960f5a546aedf317ad59e94 /pretyping/detyping.ml | |
| parent | 903fe285c008389982d292a494c39ed99aa3e0b5 (diff) | |
Typo resulting in bad eta-expansion of destructing let's body.
Revealed by message on coq-club on 24/11/2013.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bdbfe412e..4e0fc5de6 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -305,7 +305,7 @@ let it_destRLambda_or_LetIn_names n c = let a = GVar (dl,x) in aux (n-1) (Name x :: nal) (match c with - | GApp (loc,p,l) -> GApp (loc,c,l@[a]) + | GApp (loc,p,l) -> GApp (loc,p,l@[a]) | _ -> (GApp (dl,c,[a]))) in aux n [] c |