From a5d124dd7c3d43a5ead81cfac30c7d1448002d56 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Nov 2019 15:53:48 +0100
Subject: Fix #11039: proof of False with template poly and nonlinear universes

Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.

A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.

Also fixes #10504.
---
 plugins/ssr/ssrbool.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index f6b192c226..475859fcc2 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -1184,7 +1184,6 @@ Notation xpreim := (fun f (p : pred _) x => p (f x)).
 
 (** The packed class interface for pred-like types. **)
 
-#[universes(template)]
 Structure predType T :=
    PredType {pred_sort :> Type; topred : pred_sort -> pred T}.
 
-- 
cgit v1.2.3