Renaming variants of Entries.local_entry

The original datatype:

  Entries.local_entry = LocalDef of constr
                      | LocalAssum of constr

was changed to:

  Entries.local_entry = LocalDefEntry of constr
                      | LocalAssumEntry of constr

There are two advantages:

  1. the new names are consistent with other variant names in the same module
     which also have this "*Entry" suffix
  2. the new names do not collide with variants defined in the Context.{Rel,Named}.Declaration
     modules so both, "Entries" as well as "Context.{Rel,Named}.Declaration" can be open at the same time.

The disadvantage is that those new variants are longer.
But since those variants are rarely used, it it is not a big deal.

0 files changed, 0 insertions, 0 deletions