diff options
| author | Maxime Dénès | 2018-03-04 16:32:21 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:32:21 +0100 |
| commit | 97f4f3cc0425b62b1e23454dca85a10eea605ef5 (patch) | |
| tree | 3f7715946b597188bc78d2e15c9582b36e3e63fc | |
| parent | 346e73cef9e4e89c90f9f6f7011d54e3a0a35d96 (diff) | |
| parent | 01cf21509667263c2067cb87e2b2f604c4f9cb1e (diff) | |
Merge PR #6879: 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 f1e8d10317..5dca69c165 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 0000000000..70f1b3127a --- /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. |