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

17 files changed, 89 insertions, 98 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 =
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).
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index b4300da4d5..3736bc47a5 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -730,7 +730,6 @@ Qed.
 
 (* The input: syntax of a field expression *)
 
-#[universes(template)]
 Inductive FExpr : Type :=
  | FEO : FExpr
  | FEI : FExpr
@@ -763,7 +762,6 @@ Strategy expand [FEeval].
 
 (* The result of the normalisation *)
 
-#[universes(template)]
 Record linear : Type := mk_linear {
    num : PExpr C;
    denum : PExpr C;
@@ -946,7 +944,6 @@ induction e2; intros p1 p2;
   now rewrite <- PEpow_mul_r.
 Qed.
 
-#[universes(template)]
 Record rsplit : Type := mk_rsplit {
    rsplit_left : PExpr C;
    rsplit_common : PExpr C;
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index b024f65988..a98a963207 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -740,7 +740,6 @@ Ltac abstract_ring_morphism set ext rspec :=
   | _ => fail 1 "bad ring structure"
   end.
 
-#[universes(template)]
 Record hypo : Type := mkhypo {
    hypo_type : Type;
    hypo_proof : hypo_type
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 6a8c514a7b..048c8eecf9 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -32,7 +32,6 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.
    with coefficients in C :
  *)
 
-#[universes(template)]
  Inductive Pol : Type :=
   | Pc : C -> Pol
   | PX : Pol -> positive -> positive -> Pol -> Pol. 
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 9d56084fd4..092114ff0b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -121,7 +121,6 @@ Section MakeRingPol.
     - (Pinj i (Pc c)) is (Pc c)
  *)
 
- #[universes(template)]
  Inductive Pol : Type :=
   | Pc : C -> Pol
   | Pinj : positive -> Pol -> Pol
@@ -909,7 +908,6 @@ Section MakeRingPol.
 
  (** Definition of polynomial expressions *)
 
- #[universes(template)]
  Inductive PExpr : Type :=
   | PEO : PExpr
   | PEI : PExpr            
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 8f24b281c6..dc45853458 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -540,7 +540,6 @@ Section AddRing.
  Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
  Variable req : R -> R -> Prop. *)
 
-#[universes(template)]
 Inductive ring_kind : Type :=
 | Abstract
 | Computational
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index eb75fca0a1..b456d2eed2 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -151,7 +151,7 @@ let ic_unsafe c = (*FIXME remove *)
 let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
-  let univs = UState.restrict_universe_context univs vars in
+  let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
   let () = Declare.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index bf0761d3ae..376410658a 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -1323,7 +1323,6 @@ Proof. by move=> x y r2xy; apply/orP; right. Qed.
 
 (** Variant of simpl_pred specialised to the membership operator. **)
 
-#[universes(template)]
 Variant mem_pred T := Mem of pred T.
 
 (**
@@ -1464,7 +1463,6 @@ Implicit Types (mp : mem_pred T).
    Definition Acoll : collective_pred T := [pred x | ...].
  as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl.  **)
 
-#[universes(template)]
 Structure registered_applicative_pred p := RegisteredApplicativePred {
   applicative_pred_value :> pred T;
   _ : applicative_pred_value = p
@@ -1473,21 +1471,18 @@ Definition ApplicativePred p := RegisteredApplicativePred (erefl p).
 Canonical applicative_pred_applicative sp :=
   ApplicativePred (applicative_pred_of_simpl sp).
 
-#[universes(template)]
 Structure manifest_simpl_pred p := ManifestSimplPred {
   simpl_pred_value :> simpl_pred T;
   _ : simpl_pred_value = SimplPred p
 }.
 Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
 
-#[universes(template)]
 Structure manifest_mem_pred p := ManifestMemPred {
   mem_pred_value :> mem_pred T;
   _ : mem_pred_value = Mem [eta p]
 }.
 Canonical expose_mem_pred p := ManifestMemPred (erefl (Mem [eta p])).
 
-#[universes(template)]
 Structure applicative_mem_pred p :=
   ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
 Canonical check_applicative_mem_pred p (ap : registered_applicative_pred p) :=
@@ -1538,7 +1533,6 @@ End PredicateSimplification.
 
 (**  Qualifiers and keyed predicates.  **)
 
-#[universes(template)]
 Variant qualifier (q : nat) T := Qualifier of {pred T}.
 
 Coercion has_quality n T (q : qualifier n T) : {pred T} :=
@@ -1573,7 +1567,6 @@ Variable T : Type.
 Variant pred_key (p : {pred T}) := DefaultPredKey.
 
 Variable p : {pred T}.
-#[universes(template)]
 Structure keyed_pred (k : pred_key p) :=
   PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}.
 
@@ -1605,7 +1598,6 @@ Section KeyedQualifier.
 
 Variables (T : Type) (n : nat) (q : qualifier n T).
 
-#[universes(template)]
 Structure keyed_qualifier (k : pred_key q) :=
   PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}.
 Definition KeyedQualifier k := PackKeyedQualifier k (erefl q).
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 71abafc22f..9ebdf71329 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -209,7 +209,6 @@ Register abstract_key as plugins.ssreflect.abstract_key.
 Register abstract as plugins.ssreflect.abstract.
 
 (**  Constants for tactic-views  **)
-#[universes(template)]
 Inductive external_view : Type := tactic_view of Type.
 
 (**
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 5e600362b4..0ce3752a51 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -391,19 +391,19 @@ Notation "@^~ x" := (fun f => f x) : fun_scope.
  Definitions and notation for explicit functions with simplification,
  i.e., which simpl and /= beta expand (this is complementary to nosimpl).  **)
 
+#[universes(template)]
+Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT.
+
 Section SimplFun.
 
 Variables aT rT : Type.
 
-#[universes(template)]
-Variant simpl_fun := SimplFun of aT -> rT.
+Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x.
 
-Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
+End SimplFun.
 
 Coercion fun_of_simpl : simpl_fun >-> Funclass.
 
-End SimplFun.
-
 Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope.
 Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope.
 Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope.