diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-16 07:38:45 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-16 07:38:45 +0100 |
| commit | 1dddd062f35736285eb2940382df2b53224578a7 (patch) | |
| tree | 55eb10f5422da4474bf482ae1dbe84a4a490a37d /toplevel/discharge.ml | |
| parent | 13e847b7092d53ffec63e4cba54c67d39560e67a (diff) | |
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.
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 5fa51e06e..ffa11679c 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -14,6 +14,7 @@ open Vars open Entries open Declarations open Cooking +open Entries open Context.Rel.Declaration (********************************) @@ -21,8 +22,8 @@ open Context.Rel.Declaration let detype_param = function - | LocalAssum (Name id, p) -> id, Entries.LocalAssum p - | LocalDef (Name id, p,_) -> id, Entries.LocalDef p + | LocalAssum (Name id, p) -> id, LocalAssumEntry p + | LocalDef (Name id, p,_) -> id, LocalDefEntry p | _ -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace |