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/rtauto/Bintree.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 99c02995fb..751f0d8334 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -81,10 +81,12 @@ Section Store.
 
 Variable A:Type.
 
+#[universes(template)]
 Inductive Poption : Type:=
   PSome : A -> Poption
 | PNone : Poption.
 
+#[universes(template)]
 Inductive Tree : Type :=
    Tempty : Tree
  | Branch0 : Tree -> Tree -> Tree
@@ -177,6 +179,7 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*;
 destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
 Qed.
 
+#[universes(template)]
 Record Store : Type :=
 mkStore  {index:positive;contents:Tree}.
 
@@ -191,6 +194,7 @@ Lemma get_empty : forall i, get i empty = PNone.
 intro i; case i; unfold empty,get; simpl;reflexivity.
 Qed.
 
+#[universes(template)]
 Inductive Full : Store -> Type:=
     F_empty : Full empty
   | F_push : forall a S, Full S -> Full (push a S).
-- 
cgit v1.2.3