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.
---
 theories/Program/Equality.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index b09a7d3264..c5165662e5 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -257,7 +257,6 @@ Ltac blocked t := block_goal ; t ; unblock_goal.
    be used by the [equations] resolver. It is especially useful to register the dependent elimination
    principles for things in [Prop] which are not automatically generated. *)
 
-#[universes(template)]
 Class DependentEliminationPackage (A : Type) :=
   { elim_type : Type ; elim : elim_type }.
 
-- 
cgit v1.2.3