aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-08-31 17:40:28 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-03 13:39:18 +0200
commit6ba75b01a7e39f48a325b04fd891939927b981da (patch)
tree3725d6f85e58a5d5b5707607ca3727030fd87434
parentc11bd7b181d6e53910dc8d39c5360f35c7b24674 (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.ml4
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 ->