diff options
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 |