Update the name cache when creating new names via DeriveGeneric
New external top-level names were being created but the name cache
wasn't being populated, leading to #7878.
Signed-off-by:
Jose Pedro Magalhaes <jpm@cs.ox.ac.uk>
Loading
Please register or sign in to comment