aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/namegen.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-11 12:27:19 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-11 12:51:20 +0200
commit484c18b44c19bb139a4c574250d9913cc347ed5a (patch)
tree224f5ca2446809b5d2b704fd2666f02f311e08e9 /engine/namegen.ml
parentefca6e2f2268a6ff0a7c06ff28fffd02243f02c1 (diff)
CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function
Diffstat (limited to 'engine/namegen.ml')
-rw-r--r--engine/namegen.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 8a766a717..129cb3868 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -287,8 +287,7 @@ let make_all_name_different env =
let avoid = ref (ids_of_named_context (named_context env)) in
process_rel_context
(fun decl newenv ->
- let (na,_,t) = to_tuple decl in
- let na = named_hd newenv t na in
+ let na = named_hd newenv (get_type decl) (get_name decl) in
let id = next_name_away na !avoid in
avoid := id::!avoid;
push_rel (set_name (Name id) decl) newenv)