diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 17:40:28 +0200 |
|---|---|---|
| committer |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:39:18 +0200 |
| commit | 6ba75b01a7e39f48a325b04fd891939927b981da (patch) | |
| tree | 3725d6f85e58a5d5b5707607ca3727030fd87434 | |
| parent | c11bd7b181d6e53910dc8d39c5360f35c7b24674 (diff) | |
Term_typing: remove unused argument to internal function.
The function is defined with a typo but called with the same env that
is mistakenly not shadowed.
An alternative to this commit would be to fix the typo.
| -rw-r--r-- | kernel/term_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 30127d166..1f7ee145a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -378,7 +378,7 @@ let build_constant_declaration kn env result = str "Proof using " ++ declared_vars ++ fnl () ++ str "to" ++ fnl () ++ str "Proof using " ++ inferred_vars) in - let sort evn l = + let sort l = List.filter (fun decl -> let id = NamedDecl.get_id decl in List.exists (NamedDecl.get_id %> Names.Id.equal id) l) @@ -411,7 +411,7 @@ let build_constant_declaration kn env result = [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) - sort env declared, + sort declared, match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> |