diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-01 14:32:04 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-01 14:33:28 +0100 |
| commit | 01cf21509667263c2067cb87e2b2f604c4f9cb1e (patch) | |
| tree | 8233b6fa643e289e98afe217931dd4558f81953e /kernel/uGraph.ml | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Fix #6878: univ undefined for [with Definition] bad instance size.
Diffstat (limited to 'kernel/uGraph.ml')
| -rw-r--r-- | kernel/uGraph.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index f1e8d1031..5dca69c16 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -833,7 +833,7 @@ let sort_universes g = (** Subtyping of polymorphic contexts *) let check_subtype univs ctxT ctx = - if AUContext.size ctx == AUContext.size ctx then + if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in let push accu v = add_universe v false accu in |