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 | |
parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) |
Fix #6878: univ undefined for [with Definition] bad instance size.
-rw-r--r-- | kernel/uGraph.ml | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/6878.v | 8 |
2 files changed, 9 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 diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v new file mode 100644 index 000000000..70f1b3127 --- /dev/null +++ b/test-suite/bugs/closed/6878.v @@ -0,0 +1,8 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo : Prop. +End T. + +(** Used to anomaly *) +Fail Module M : T with Definition foo := Type. |