diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 8201980e3..b303a1a5a 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -977,7 +977,7 @@ let eq_puniverses f (x, u) (y, u') = f x y && Instance.equal u u' (** A context of universe levels with universe constraints, - representiong local universe variables and constraints *) + representing local universe variables and constraints *) module UContext = struct @@ -1001,8 +1001,11 @@ struct let union (univs, cst) (univs', cst') = Instance.append univs univs', Constraint.union cst cst' - + let dest x = x + + let size (x,_) = Instance.length x + end type universe_context = UContext.t |