diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/Bintree.v | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 0ca0d0c12d..6b92445326 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -77,20 +77,24 @@ Lget i (l ++ delta) = Some a. induction l;destruct i;simpl;try congruence;auto. Qed. -Section Store. - -Variable A:Type. - -#[universes(template)] -Inductive Poption : Type:= +Inductive Poption {A} : Type:= PSome : A -> Poption | PNone : Poption. +Arguments Poption : clear implicits. -#[universes(template)] -Inductive Tree : Type := +Inductive Tree {A} : Type := Tempty : Tree | Branch0 : Tree -> Tree -> Tree | Branch1 : A -> Tree -> Tree -> Tree. +Arguments Tree : clear implicits. + +Section Store. + +Variable A:Type. + +Notation Poption := (Poption A). +Notation Tree := (Tree A). + Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := match T with @@ -179,7 +183,6 @@ 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}. @@ -194,7 +197,6 @@ 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). |