diff options
| author | Gaëtan Gilbert | 2018-09-15 20:09:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-19 17:02:45 +0100 |
| commit | 8202a6394425bfd8db22966fe0ef83441d7b5d04 (patch) | |
| tree | 41387774232caf0b7eec63bdca8ee315d35f6ad6 /plugins/rtauto | |
| parent | 7492a1ae8422b3f996f844ae96376c3f88d82e13 (diff) | |
Put #[universes(template)] on all auto template spots in stdlib
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/Bintree.v | 4 |
1 files changed, 4 insertions, 0 deletions
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). |