diff options
Diffstat (limited to 'kernel')
| -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 |