diff options
| author | Pierre-Marie Pédrot | 2018-09-12 11:42:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 4c28e0597067d81f5ee7e8b2b2e668f4d45e973f (patch) | |
| tree | d29d77f567b7289fbb2fede3a18dae58c50a7dac /kernel/univ.ml | |
| parent | 90ace7786901aa2f1253cf3887bf3e5221c5dae7 (diff) | |
Fix printing of abstract universe contexts.
Due to their representation using names, the instance was not properly
displayed.
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 311477daca..8acbeb2d25 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -954,6 +954,8 @@ struct let repr (inst, cst) = (Array.mapi (fun i l -> Level.var i) inst, cst) + let pr f ?variance ctx = pr f ?variance (repr ctx) + let instantiate inst (u, cst) = assert (Array.length u = Array.length inst); subst_instance_constraints inst cst |