diff options
| author | Matthieu Sozeau | 2014-07-01 22:50:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-01 22:52:08 +0200 |
| commit | 4c97e4ce19ca4c387039cfdcb4f24658100230b0 (patch) | |
| tree | 8e6367b1936d842b3e56283abc25de2342452884 /kernel | |
| parent | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff) | |
Add toplevel commands to declare global universes and constraints.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 11 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 |
2 files changed, 13 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 1e7d2c83cb..b42de5a760 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -539,6 +539,10 @@ struct let pr x = str(to_string x) + let pr_with f (v, n) = + if Int.equal n 0 then f v + else f v ++ str"+" ++ int n + let is_level = function | (v, 0) -> true | _ -> false @@ -591,6 +595,13 @@ struct str "max(" ++ hov 0 (prlist_with_sep pr_comma Expr.pr (to_list l)) ++ str ")" + + let pr_with f l = match node l with + | Cons (u, n) when is_nil n -> Expr.pr_with f u + | _ -> + str "max(" ++ hov 0 + (prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++ + str ")" let atom l = match node l with | Cons (l, n) when is_nil n -> Some l diff --git a/kernel/univ.mli b/kernel/univ.mli index 832da157e3..8166d75e62 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -79,6 +79,8 @@ sig val pr : t -> Pp.std_ppcmds (** Pretty-printing *) + val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) |