diff options
Diffstat (limited to 'library/misctypes.ml')
| -rw-r--r-- | library/misctypes.ml | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/library/misctypes.ml b/library/misctypes.ml index 72db3b31cb..cfae074843 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -50,39 +50,10 @@ 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 -(** Case style, shared with Term *) - -type case_style = Constr.case_style = - | LetStyle - | IfStyle - | LetPatternStyle - | MatchStyle - | RegularStyle (** infer printing form from number of constructor *) -[@@ocaml.deprecated "Alias for Constr.case_style"] - (** Casts *) type 'a cast_type = @@ -141,9 +112,3 @@ type multi = | UpTo of int | RepeatStar | RepeatPlus - -type ('a, 'b) gen_universe_decl = { - univdecl_instance : 'a; (* Declared universes *) - univdecl_extensible_instance : bool; (* Can new universes be added *) - univdecl_constraints : 'b; (* Declared constraints *) - univdecl_extensible_constraints : bool (* Can new constraints be added *) } |