diff options
| author | Gaëtan Gilbert | 2018-04-28 21:27:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-17 18:47:10 +0200 |
| commit | 302adae094bbf76d8c951c557c85acb12a97aedc (patch) | |
| tree | 66e3cfab6cf5cda2f51a18308a5e893d621d21ae /engine/termops.ml | |
| parent | dc7696652ccd23887a474f3d4141b1850e51d46f (diff) | |
Split off Universes functions about substitutions and constraints
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 9e975da58c..c271d9d999 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -306,7 +306,7 @@ let pr_evar_universe_context ctx = str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ str "WEAK CONSTRAINTS:"++brk(0,1)++ h 0 (UState.pr_weak prl ctx) ++ fnl ()) |