diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-24 03:26:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 01:13:04 +0200 |
| commit | a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f (patch) | |
| tree | 911c09c586a6d90a6d1e304e86260767a7b0bdbb /library | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
[api] Move universe syntax to `Glob_term`
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
Diffstat (limited to 'library')
| -rw-r--r-- | library/misctypes.ml | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/library/misctypes.ml b/library/misctypes.ml index 72db3b31c..b5d30559d 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -50,25 +50,6 @@ type 'id move_location = | MoveFirst | MoveLast (** can be seen as "no move" when doing intro *) -(** Sorts *) - -type 'a glob_sort_gen = - | GProp (** representation of [Prop] literal *) - | GSet (** representation of [Set] literal *) - | GType of 'a (** representation of [Type] literal *) - -type 'a universe_kind = - | UAnonymous - | UUnknown - | UNamed of 'a - -type level_info = Libnames.reference universe_kind -type glob_level = level_info glob_sort_gen -type glob_constraint = glob_level * Univ.constraint_type * glob_level - -type sort_info = (Libnames.reference * int) option list -type glob_sort = sort_info glob_sort_gen - (** A synonym of [Evar.t], also defined in Term *) type existential_key = Evar.t |