Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

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