From 8202a6394425bfd8db22966fe0ef83441d7b5d04 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 15 Sep 2018 20:09:15 +0200
Subject: Put #[universes(template)] on all auto template spots in stdlib

---
 theories/Program/Equality.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index cf42ed18db..5ae933d433 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -257,6 +257,7 @@ 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