diff options
| author | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
| commit | 083e83a2e82c17c13b5af7d59029d4ef0aa1b613 (patch) | |
| tree | 7609e9b92c93fe21603aaa2f7d90805e30812f53 /kernel/reduction.ml | |
| parent | 1f74267d7e4affe14dbafc1a6f1e6f3f465f75a8 (diff) | |
| parent | 24a9a9c4bef18133c0b5070992d3396ff7596a7c (diff) | |
Merge PR #9918: Fix #9294: critical bug with template polymorphism
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 53f228c618..327cb2efeb 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u - | Type _u, Prop -> raise NotConvertible + | Type u, Prop -> infer_pb u Univ.type0m_univ | Type u, Set -> infer_pb u Univ.type0_univ | Type u0, Type u1 -> infer_pb u0 u1 |