diff options
Diffstat (limited to 'library/misctypes.ml')
| -rw-r--r-- | library/misctypes.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/library/misctypes.ml b/library/misctypes.ml index a3c887045..cfae07484 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -112,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 *) } |