diff options
| author | Hugo Herbelin | 2013-11-25 14:14:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2013-11-25 14:28:06 +0100 |
| commit | 32c900252a07ea7d2dd9fe15feb21ef98aee3df7 (patch) | |
| tree | f0ded05c6d99135fa960f5a546aedf317ad59e94 | |
| parent | 903fe285c008389982d292a494c39ed99aa3e0b5 (diff) | |
Typo resulting in bad eta-expansion of destructing let's body.
Revealed by message on coq-club on 24/11/2013.
| -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 bdbfe412e7..4e0fc5de69 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 |