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

22 files changed, 52 insertions, 74 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 428af5fcfe..69bd1e6c96 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -286,7 +286,6 @@ Local Open Scope list_scope.
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
 (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *)
-#[universes(template)]
 Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist.
 Local Infix "::" := Tcons.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 071810acdc..6858706cb3 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -27,7 +27,6 @@ Require Export Coq.Classes.Morphisms.
 
 (** A setoid wraps an equivalence. *)
 
-#[universes(template)]
 Class Setoid A := {
   equiv : relation A ;
   setoid_equiv :> Equivalence equiv }.
@@ -129,7 +128,6 @@ Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (
 
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
-#[universes(template)]
 Class PartialSetoid (A : Type) :=
   { pequiv : relation A ; pequiv_prf :> PER pequiv }.
 
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index 5025bce093..274cb4afd3 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -14,3 +14,6 @@ Local Set Warnings "-deprecated".
 Require Export Coq.Compat.Coq810.
 
 Unset Private Polymorphic Universes.
+
+(** Unsafe flag, can hide inconsistencies. *)
+Global Unset Template Check.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 801be79ba4..8627ff7353 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -45,20 +45,23 @@ Hint Transparent key : core.
 
 (** * Trees *)
 
-Section Elt.
-
-Variable elt : Type.
-
 (** * Trees
 
    The fifth field of [Node] is the height of the tree *)
 
 #[universes(template)]
-Inductive tree :=
+Inductive tree {elt : Type} :=
   | Leaf : tree
   | Node : tree -> key -> elt -> tree -> int -> tree.
+Arguments tree : clear implicits.
 
-Notation t := tree.
+Section Elt.
+
+Variable elt : Type.
+
+Notation t := (tree elt).
+
+Implicit Types m : t.
 
 (** * Basic functions on trees: height and cardinal *)
 
@@ -76,7 +79,7 @@ Fixpoint cardinal (m : t) : nat :=
 
 (** * Empty Map *)
 
-Definition empty := Leaf.
+Definition empty : t := Leaf.
 
 (** * Emptyness test *)
 
@@ -236,7 +239,6 @@ Fixpoint join l : key -> elt -> t -> t :=
     - [o] is the result of [find x m].
 *)
 
-#[universes(template)]
 Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }.
 Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 
@@ -293,7 +295,6 @@ Variable cmp : elt->elt->bool.
 
 (** ** Enumeration of the elements of a tree *)
 
-#[universes(template)]
 Inductive enumeration :=
  | End : enumeration
  | More : key -> elt -> t -> enumeration -> enumeration.
@@ -338,6 +339,9 @@ Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End).
 
 End Elt.
 Notation t := tree.
+Arguments Leaf : clear implicits.
+Arguments Node [elt].
+
 Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 Notation "t #l" := (t_left t) (at level 9, format "t '#l'").
 Notation "t #o" := (t_opt t) (at level 9, format "t '#o'").
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 2af6e5c6a4..b21d809059 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -1024,7 +1024,6 @@ Module E := X.
 
 Definition key := E.t.
 
-#[universes(template)]
 Record slist (elt:Type) :=
   {this :> Raw.t elt; sorted : sort (@Raw.PX.ltk elt) this}.
 Definition t (elt:Type) : Type := slist elt.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0c04437581..b9a8b0a73d 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -868,8 +868,6 @@ Module Make (X: DecidableType) <: WS with Module E:=X.
 
  Module E := X.
  Definition key := E.t.
-
-#[universes(template)]
  Record slist (elt:Type) :=
   {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}.
  Definition t (elt:Type) := slist elt.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 1639115cbd..3e0bf1d8ae 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -387,8 +387,10 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined.
 (** [identity A a] is the family of datatypes on [A] whose sole non-empty
     member is the singleton datatype [identity A a a] whose
     sole inhabitant is denoted [identity_refl A a] *)
+(** Beware: this inductive actually falls into [Prop], as the sole
+    constructor has no arguments and [-indices-matter] is not
+    activated in the standard library. *)
 
-#[universes(template)]
 Inductive identity (A:Type) (a:A) : A -> Type :=
   identity_refl : identity a a.
 Hint Resolve identity_refl: core.
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index c11a0941fa..4c6520feb3 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -73,14 +73,17 @@ End MemoFunction.
     reused thanks to a temporary hiding of the dependency
     in a "container" [memo_val]. *)
 
+#[universes(template)]
+Inductive memo_val {A : nat -> Type} : Type :=
+  memo_mval: forall n, A n -> memo_val.
+Arguments memo_val : clear implicits.
+
 Section DependentMemoFunction.
 
 Variable A: nat -> Type.
 Variable f: forall n, A n.
 
-#[universes(template)]
-Inductive memo_val: Type :=
-  memo_mval: forall n, A n -> memo_val.
+Notation memo_val := (memo_val A).
 
 Fixpoint is_eq (n m : nat) : {n = m} + {True} :=
   match n, m return {n = m} + {True} with
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 407a7ae45d..0daae0391c 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -12,13 +12,13 @@ Set Implicit Arguments.
 
 (** Streams *)
 
-Section Streams.
+CoInductive Stream (A : Type) :=
+  Cons : A -> Stream A -> Stream A.
 
-Variable A : Type.
+Section Streams.
+  Variable A : Type.
 
-#[universes(template)]
-CoInductive Stream : Type :=
-    Cons : A -> Stream -> Stream.
+  Notation Stream := (Stream A).
 
 
 Definition hd (x:Stream) := match x with
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 4442108ffc..8a71158f4c 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -208,7 +208,6 @@ Definition concat s1 s2 :=
     - [present] is [true] if and only if [s] contains  [x].
 *)
 
-#[universes(template)]
 Record triple := mktriple { t_left:t; t_in:bool; t_right:t }.
 Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 37a169b02e..bf6336ae47 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -48,7 +48,6 @@ Module Type Ops (X:OrderedType)(Info:InfoTyp).
 Definition elt := X.t.
 Hint Transparent elt : core.
 
-#[universes(template)]
 Inductive tree  : Type :=
 | Leaf : tree
 | Node : Info.t -> tree -> X.t -> tree -> tree.
@@ -168,7 +167,6 @@ end.
 (** Enumeration of the elements of a tree. This corresponds
     to the "samefringe" notion in the literature. *)
 
-#[universes(template)]
 Inductive enumeration :=
  | End : enumeration
  | More : elt -> tree -> enumeration -> enumeration.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 29c84d0d1a..33f6b1050c 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -439,7 +439,6 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
 
  Definition elt := E.t.
 
-#[universes(template)]
  Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
  Definition t := t_.
  Arguments Mkt this {is_ok}.
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v
index 83e9c29b13..6e08378df4 100644
--- a/theories/Numbers/Cyclic/Abstract/DoubleType.v
+++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v
@@ -18,46 +18,34 @@ Local Open Scope Z_scope.
 Definition base digits := Z.pow 2 (Zpos digits).
 Arguments base digits: simpl never.
 
-Section Carry.
+#[universes(template)]
+Variant carry (A : Type) :=
+| C0 : A -> carry A
+| C1 : A -> carry A.
 
- Variable A : Type.
-
- #[universes(template)]
- Variant carry :=
-  | C0 : A -> carry
-  | C1 : A -> carry.
-
- Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c :=
+Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c :=
   match c with
   | C0 x => interp x
   | C1 x => sign*B + interp x
   end.
 
-End Carry.
-
-Section Zn2Z.
-
- Variable znz : Type.
-
- (** From a type [znz] representing a cyclic structure Z/nZ,
-     we produce a representation of Z/2nZ by pairs of elements of [znz]
-     (plus a special case for zero). High half of the new number comes
-     first.
+(** From a type [znz] representing a cyclic structure Z/nZ,
+    we produce a representation of Z/2nZ by pairs of elements of [znz]
+    (plus a special case for zero). High half of the new number comes
+    first.
  *)
+#[universes(template)]
+Variant zn2z {znz : Type} :=
+| W0 : zn2z
+| WW : znz -> znz -> zn2z.
+Arguments zn2z : clear implicits.
 
- #[universes(template)]
- Variant zn2z :=
-  | W0 : zn2z
-  | WW : znz -> znz -> zn2z.
-
- Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) :=
+Definition zn2z_to_Z znz (wB:Z) (w_to_Z:znz->Z) (x:zn2z znz) :=
   match x with
   | W0 => 0
   | WW xh xl => w_to_Z xh * wB + w_to_Z xl
   end.
 
-End Zn2Z.
-
 Arguments W0 {znz}.
 
 (** From a cyclic representation [w], we iterate the [zn2z] construct
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 128ee286b8..6da0fe3966 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -137,7 +137,6 @@ Definition IsStepFun (f:R -> R) (a b:R) : Type :=
   { l:Rlist & is_subdivision f a b l }.
 
 (** ** Class of step functions *)
-#[universes(template)]
 Record StepFun (a b:R) : Type := mkStepFun
   {fe :> R -> R; pre : IsStepFun fe a b}.
 
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 5443ff68ed..c94a373ca0 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -116,7 +116,6 @@ Qed.
 (*******************************)
 
 (*********)
-#[universes(template)]
 Record Metric_Space : Type :=
   {Base : Type;
     dist : Base -> Base -> R;
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index cfcc82d765..d21042884e 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -380,7 +380,6 @@ Proof.
   apply Rinv_0_lt_compat; prove_sup0.
 Qed.
 
-#[universes(template)]
 Record family : Type := mkfamily
   {ind : R -> Prop;
     f :> R -> R -> Prop;
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index e1d7d37e42..745db25a54 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -100,11 +100,9 @@ Hint Resolve Totally_ordered_definition Upper_Bound_definition
 Section Specific_orders.
   Variable U : Type.
 
-  #[universes(template)]
   Record Cpo : Type := Definition_of_cpo
     {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
 
-  #[universes(template)]
   Record Chain : Type := Definition_of_chain
     {PO_of_chain : PO U;
     Chain_cond : Totally_ordered U PO_of_chain (@Carrier_of _ PO_of_chain)}.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index e9233a34e7..6aefcf32c0 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -22,7 +22,6 @@ Section multiset_defs.
   Hypothesis eqA_equiv : Equivalence eqA.
   Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
-  #[universes(template)]
   Inductive multiset : Type :=
     Bag : (A -> nat) -> multiset.
 
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index d2fae6db28..e23d9c2f55 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -36,7 +36,6 @@ Section Partial_orders.
 
   Definition Rel := Relation U.
 
-  #[universes(template)]
   Record PO : Type := Definition_of_PO
     { Carrier_of : Ensemble U;
       Rel_of : Relation U;
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 76e555ed5a..48a852052e 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -42,7 +42,6 @@ Section defs.
   Let emptyBag := EmptyBag A.
   Let singletonBag := SingletonBag _ eqA_dec.
 
-  #[universes(template)]
   Inductive Tree :=
     | Tree_Leaf : Tree
     | Tree_Node : A -> Tree -> Tree -> Tree.
@@ -129,8 +128,7 @@ Section defs.
 
   (** ** Merging two sorted lists *)
 
-  #[universes(template)]
-  Inductive merge_lem (l1 l2:list A) : Type :=
+   Inductive merge_lem (l1 l2:list A) : Type :=
     merge_exist :
     forall l:list A,
       Sorted leA l ->
@@ -203,7 +201,6 @@ Section defs.
 
   (** ** Specification of heap insertion *)
 
-  #[universes(template)]
   Inductive insert_spec (a:A) (T:Tree) : Type :=
     insert_exist :
     forall T1:Tree,
@@ -237,7 +234,6 @@ Section defs.
 
   (** ** Building a heap from a list *)
 
-  #[universes(template)]
   Inductive build_heap (l:list A) : Type :=
     heap_exist :
     forall T:Tree,
@@ -262,7 +258,6 @@ Section defs.
 
   (** ** Building the sorted list *)
 
-  #[universes(template)]
   Inductive flat_spec (T:Tree) : Type :=
     flat_exist :
     forall l:list A,
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index d747258f56..6ddbc8e214 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -14,17 +14,18 @@
 
 Require Import Eqdep.
 
+#[universes(template)]
+Inductive WO (A : Type) (B : A -> Type) : Type :=
+  sup : forall (a:A) (f:B a -> WO A B), WO A B.
+
 Section WellOrdering.
   Variable A : Type.
   Variable B : A -> Type.
 
-  #[universes(template)]
-  Inductive WO : Type :=
-    sup : forall (a:A) (f:B a -> WO), WO.
-
+  Notation WO := (WO A B).
 
   Inductive le_WO : WO -> WO -> Prop :=
-    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f).
+    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup _ _ a f).
 
   Theorem wf_WO : well_founded le_WO.
   Proof.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 577544f971..fee928430c 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -212,7 +212,6 @@ Module MoreInt (Import I:Int).
     | EZofI : ExprI -> ExprZ
     | EZraw : Z -> ExprZ.
 
-  #[universes(template)]
   Inductive ExprP : Type :=
     | EPeq : ExprZ -> ExprZ -> ExprP
     | EPlt : ExprZ -> ExprZ -> ExprP