Make kernel parametric on the lowest universe and fix #9294

This could be Prop (for compat with usual Coq), Set (for HoTT),
 or actually an arbitrary "i".

Take lower bound of universes into account in pretyping/engine

Reinstate proper elaboration of SProp <= l constraints:

replacing is_small with equality with lbound is _not_ semantics preserving!

lbound = Set

Elaborate template polymorphic inductives with lower bound Prop

This will make more constraints explicit

Check univ constraints with Prop as lower bound for template inductives

Restrict template polymorphic universes to those not bounded from below

Fixes #9294

fix suggested by Matthieu

Try second fix suggested by Matthieu

Take care of modifying elaboration for record declarations as well.

Rebase and export functions for debug

Remove exported functions used while debugging

Add a new typing flag "check_template" and option "-no-template-checl"

This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).

Update checker to the new typing flags structure

Switch on the new template_check flag to allow old unsafe behavior in
indTyping.

This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.

Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while

Fix `Template Check` option name and test it

Add `Unset Template Check` to Coq89.v

Cooking of inductives and template-check tests

Cleanup test-suite file for template check / universes(template) flags

cookind tests

Move test of `Unset Template Check` to the failure/ dir, but comment it
for now

Template test-suite test explanation

Overlays for PR 9918

Overlay for paramcoq

Add overlay for fiat_parsers (-no-template-check)

Add overlay for fiat_crypto_legacy

Update fiat-crypto legacy overlay

Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.

Remove overlay that should no longer be necessary

The setting in the compat file should handle it

Remove now-merged fiat-crypto-legacy overlay

Update `Print Assumptions` to reflect the typing flag for template checking

Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic

Fix pretty printing to print global universe levels properly

Fix printing of template polymorphic universes

Fix pretty printing for template polymorphism on no universe

Fix interaction of template check and universes(template) flag

Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe

Indtyping fixes for template polymorphic Props

Allow explicit template polymorphism again

Adapt to new indTyping interface

Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).

Fix check of meaningfullness of template polymorphism in the kernel.

It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.

Comment on identity non-template-polymorphism

Remove incorrect universes(template) attributes from ssr

simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).

Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance

Remove incorrect uses of #[universes(template)] from the stdlib

Extraction of micromega changes due to moving an ind decl out of a section

Remove incorrect uses of #[universes(template)] from plugins

Fix test-suite files, removing incorrect #[universes(template)] attributes

Remove incorrect #[universes(template)] attributes in test-suite

Fix test-suite

Remove overlays as they have been merged upstream.

7 files changed, 71 insertions, 65 deletions

diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 78bfe480b3..2762bb6b32 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -19,6 +19,47 @@ Require Export Ring_theory.
 Local Open Scope positive_scope.
 Import RingSyntax.
 
+(** Definition of polynomial expressions *)
+#[universes(template)]
+Inductive PExpr {C} : Type :=
+| PEc : C -> PExpr
+| PEX : positive -> PExpr
+| PEadd : PExpr -> PExpr -> PExpr
+| PEsub : PExpr -> PExpr -> PExpr
+| PEmul : PExpr -> PExpr -> PExpr
+| PEopp : PExpr -> PExpr
+| PEpow : PExpr -> N -> PExpr.
+Arguments PExpr : clear implicits.
+
+ (* Definition of multivariable polynomials with coefficients in C :
+    Type [Pol] represents [X1 ... Xn].
+    The representation is Horner's where a [n] variable polynomial
+    (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients
+    are polynomials with [n-1] variables (C[X2..Xn]).
+    There are several optimisations to make the repr compacter:
+    - [Pc c] is the constant polynomial of value c
+       == c*X1^0*..*Xn^0
+    - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables.
+        variable indices are shifted of j in Q.
+       == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn}
+    - [PX P i Q] is an optimised Horner form of P*X^i + Q
+        with P not the null polynomial
+       == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn}
+
+    In addition:
+    - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden
+      since they can be represented by the simpler form (PX P (i+j) Q)
+    - (Pinj i (Pinj j P)) is (Pinj (i+j) P)
+    - (Pinj i (Pc c)) is (Pc c)
+ *)
+
+#[universes(template)]
+Inductive Pol {C} : Type :=
+| Pc : C -> Pol
+| Pinj : positive -> Pol -> Pol
+| PX : Pol -> positive -> Pol -> Pol.
+Arguments Pol : clear implicits.
+
 Section MakeRingPol.
 
  (* Ring elements *)
@@ -96,33 +137,11 @@ Section MakeRingPol.
     match goal with |- ?t == _ => mul_permut_rec t end).
 
 
- (* Definition of multivariable polynomials with coefficients in C :
-    Type [Pol] represents [X1 ... Xn].
-    The representation is Horner's where a [n] variable polynomial
-    (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients
-    are polynomials with [n-1] variables (C[X2..Xn]).
-    There are several optimisations to make the repr compacter:
-    - [Pc c] is the constant polynomial of value c
-       == c*X1^0*..*Xn^0
-    - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables.
-        variable indices are shifted of j in Q.
-       == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn}
-    - [PX P i Q] is an optimised Horner form of P*X^i + Q
-        with P not the null polynomial
-       == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn}
+ Notation PExpr := (PExpr C).
+ Notation Pol := (Pol C).
 
-    In addition:
-    - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden
-      since they can be represented by the simpler form (PX P (i+j) Q)
-    - (Pinj i (Pinj j P)) is (Pinj (i+j) P)
-    - (Pinj i (Pc c)) is (Pc c)
- *)
-
- #[universes(template)]
- Inductive Pol : Type :=
-  | Pc : C -> Pol
-  | Pinj : positive -> Pol -> Pol
-  | PX : Pol -> positive -> Pol -> Pol.
+ Implicit Types pe : PExpr.
+ Implicit Types P : Pol.
 
  Definition P0 := Pc cO.
  Definition P1 := Pc cI.
@@ -152,7 +171,7 @@ Section MakeRingPol.
   | _ => Pinj j P
   end.
 
- Definition mkPinj_pred j P:=
+ Definition mkPinj_pred j P :=
   match j with
   | xH => P
   | xO j => Pinj (Pos.pred_double j) P
@@ -938,18 +957,6 @@ Qed.
  rewrite <- IHm; auto.
  Qed.
 
- (** Definition of polynomial expressions *)
-
- #[universes(template)]
- Inductive PExpr : Type :=
-  | PEc : C -> PExpr
-  | PEX : positive -> PExpr
-  | PEadd : PExpr -> PExpr -> PExpr
-  | PEsub : PExpr -> PExpr -> PExpr
-  | PEmul : PExpr -> PExpr -> PExpr
-  | PEopp : PExpr -> PExpr
-  | PEpow : PExpr -> N -> PExpr.
-
  (** evaluation of polynomial expressions towards R *)
  Definition mk_X j := mkPinj_pred j mkX.
 
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index a99f21ad47..3c72d3268f 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -68,7 +68,7 @@ Require Import EnvRing.
 Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
   match e with
     | PEc c =>  c
-    | PEX _ j =>  env j
+    | PEX j =>  env j
     | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
@@ -80,7 +80,7 @@ Lemma Qeval_expr_simpl : forall env e,
   Qeval_expr env e =
   match e with
     | PEc c =>  c
-    | PEX _ j =>  env j
+    | PEX j =>  env j
     | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 75801162a7..cddc140f51 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -289,7 +289,6 @@ destruct o' ; rewrite H1 ; now rewrite  (Rplus_0_l sor).
  now apply (Rplus_nonneg_nonneg sor).
 Qed.
 
-#[universes(template)]
 Inductive Psatz : Type :=
 | PsatzIn : nat -> Psatz
 | PsatzSquare : PolC -> Psatz
@@ -892,7 +891,7 @@ Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
     | Pc c => PEc c
     | Pinj j p => xdenorm  (Pos.add j jmp ) p
     | PX p j q   => PEadd
-      (PEmul (xdenorm jmp p) (PEpow (PEX _  jmp) (Npos j)))
+      (PEmul (xdenorm jmp p) (PEpow (PEX jmp) (Npos j)))
       (xdenorm (Pos.succ jmp) q)
   end.
 
@@ -961,7 +960,7 @@ Variable phi_C_of_S :   forall c,  phiS c =  phi (C_of_S c).
 Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
   match e with
     | PEc c => PEc (C_of_S c)
-    | PEX _ p => PEX _ p
+    | PEX p => PEX p
     | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
     | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
     | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 56032befba..d6ccf582ae 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -27,7 +27,6 @@ Section S.
   Context {AA  : Type}. (* type of annotations for atoms *)
   Context {AF  : Type}. (* type of formulae identifiers *)
 
-  #[universes(template)]
    Inductive GFormula  : Type :=
   | TT   : GFormula
   | FF   : GFormula
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 79cb6a3a3e..f93fe021f9 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -27,16 +27,18 @@ Set Implicit Arguments.
  * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up.
  *)
 
+Inductive t {A} : Type :=
+| Empty : t
+| Elt : A -> t
+| Branch : t  -> A -> t  -> t .
+Arguments t : clear implicits.
+
 Section MakeVarMap.
   
   Variable A : Type.
   Variable default : A.
 
-  #[universes(template)]
-  Inductive t  : Type :=
-  | Empty : t
-  | Elt : A -> t
-  | Branch : t  -> A -> t  -> t .
+  Notation t := (t A).
 
   Fixpoint find (vm : t) (p:positive) {struct vm} : A :=
     match vm with
@@ -49,7 +51,6 @@ Section MakeVarMap.
                       end
     end.
 
-
   Fixpoint singleton (x:positive) (v : A) : t :=
     match x with
     | xH => Elt v
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 3ea7635244..c0d22486b5 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -65,7 +65,7 @@ Qed.
 Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z :=
   match e with
     | PEc c => c
-    | PEX _ x => env x
+    | PEX x => env x
     | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2
     | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2
     | PEpow e1 n  => Z.pow (Zeval_expr env e1) (Z.of_N n)
@@ -78,7 +78,7 @@ Definition eval_expr := eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x
 Fixpoint Zeval_const  (e: PExpr Z) : option Z :=
   match e with
   | PEc c => Some c
-  | PEX _ x => None
+  | PEX x => None
   | PEadd e1 e2 => map_option2 (fun x y => Some (x + y))
                                (Zeval_const e1) (Zeval_const e2)
   | PEmul e1 e2 => map_option2 (fun x y => Some (x * y))
@@ -742,7 +742,7 @@ Module Vars.
 Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t :=
   match e with
   | PEc _ => Vars.empty
-  | PEX _ x => Vars.singleton x
+  | PEX x => Vars.singleton x
   | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 =>
     let v1 := vars_of_pexpr e1 in
     let v2 := vars_of_pexpr e2 in
@@ -774,10 +774,10 @@ Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type}
   end.
 
 Definition bound_var (v : positive) : Formula Z :=
-  Build_Formula (PEX _ v) OpGe (PEc 0).
+  Build_Formula (PEX v) OpGe (PEc 0).
 
 Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z :=
-  Build_Formula (PEX _ x) OpEq (PEsub (PEX _ y) (PEX _ t)).
+  Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)).
 
 Section BOUND.
   Context {TX TG ID : Type}.
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index a64a5a84b3..2e97dfea19 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -556,6 +556,15 @@ let zeq_bool x y =
   | Eq -> true
   | _ -> false
 
+type 'c pExpr =
+| PEc of 'c
+| PEX of positive
+| PEadd of 'c pExpr * 'c pExpr
+| PEsub of 'c pExpr * 'c pExpr
+| PEmul of 'c pExpr * 'c pExpr
+| PEopp of 'c pExpr
+| PEpow of 'c pExpr * n
+
 type 'c pol =
 | Pc of 'c
 | Pinj of positive * 'c pol
@@ -868,15 +877,6 @@ let rec psquare cO cI cadd cmul ceqb = function
   let p3 = psquare cO cI cadd cmul ceqb p2 in
   mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2
 
-type 'c pExpr =
-| PEc of 'c
-| PEX of positive
-| PEadd of 'c pExpr * 'c pExpr
-| PEsub of 'c pExpr * 'c pExpr
-| PEmul of 'c pExpr * 'c pExpr
-| PEopp of 'c pExpr
-| PEpow of 'c pExpr * n
-
 (** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **)
 
 let mk_X cO cI j =