From 6ba75b01a7e39f48a325b04fd891939927b981da Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 31 Aug 2017 17:40:28 +0200 Subject: 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. --- kernel/term_typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') 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 -> -- cgit v1.2.3