diff options
Diffstat (limited to 'engine/namegen.ml')
-rw-r--r-- | engine/namegen.ml | 3 |
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) |