diff options
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). |