Try a new way of handling template universe levels

2 files changed, 7 insertions, 7 deletions

diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 85fd810264..10d54d2283 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -588,13 +588,13 @@ Qed.
 (** Smart constructors for polynomial expression,
     with reduction of constants *)
 
-Definition NPEadd e1 e2 :=
+Time Definition NPEadd e1 e2 :=
   match e1, e2 with
   | PEc c1, PEc c2 => PEc (c1 + c2)
   | PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2
   |  _, PEc c => if (c =? 0)%coef then e1 else e1 + e2
     (* Peut t'on factoriser ici ??? *)
-  | _, _ => e1 + e2
+  | _, _ => (@PEadd C e1 e2)
   end%poly.
 Infix "++" := NPEadd (at level 60, right associativity).
 
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 1d958d09b2..8bb44ecbc7 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -240,23 +240,23 @@ Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv :=
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEadd e1 e2)
+          let e2 := mkP t2 in constr:(@PEadd C e1 e2)
         | (rmul ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEmul e1 e2)
+          let e2 := mkP t2 in constr:(@PEmul C e1 e2)
         | (rsub ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEsub e1 e2)
+          let e2 := mkP t2 in constr:(@PEsub C e1 e2)
         | (ropp ?t1) =>
           fun _ =>
-          let e1 := mkP t1 in constr:(PEopp e1)
+          let e1 := mkP t1 in constr:(@PEopp C e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant =>
             fun _ => let p := Find_at t fv in constr:(PEX C p)
-          | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(@PEpow C e1 c)
           end
         | _ =>
           fun _ => let p := Find_at t fv in constr:(PEX C p)