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

---
 plugins/setoid_ring/InitialRing.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/setoid_ring/InitialRing.v')

diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index f5db275465..15d490a6ab 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -740,6 +740,7 @@ Ltac abstract_ring_morphism set ext rspec :=
   | _ => fail 1 "bad ring structure"
   end.
 
+#[universes(template)]
 Record hypo : Type := mkhypo {
    hypo_type : Type;
    hypo_proof : hypo_type
-- 
cgit v1.2.3