diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-18 12:18:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-18 12:18:05 +0200 |
| commit | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch) | |
| tree | 01f750142359361f800e0dc2dfe422f145f491c5 /engine/namegen.ml | |
| parent | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff) | |
| parent | fdd6a17b272995237c9f95fc465bb1ff6871bedc (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine/namegen.ml')
| -rw-r--r-- | engine/namegen.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 5aca11ae6..a88c2e20e 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -278,6 +278,7 @@ let make_all_name_different env = let avoid = ref (ids_of_named_context (named_context env)) in process_rel_context (fun (na,c,t) newenv -> + let na = named_hd newenv t na in let id = next_name_away na !avoid in avoid := id::!avoid; push_rel (Name id,c,t) newenv) |