Fix Field_tac to get fast reification again, with the fix on template universe polymorphic constructors.

1 files changed, 8 insertions, 8 deletions

diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index 8ba721cb8..4ee7b99ff 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -26,37 +26,37 @@ Require Export Field_theory.
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEadd e1 e2)
+          let e2 := mkP t2 in constr:(@FEadd C e1 e2)
         | (rmul ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEmul e1 e2)
+          let e2 := mkP t2 in constr:(@FEmul C e1 e2)
         | (rsub ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEsub e1 e2)
+          let e2 := mkP t2 in constr:(@FEsub C e1 e2)
         | (ropp ?t1) =>
-          fun _ => let e1 := mkP t1 in constr:(FEopp e1)
+          fun _ => let e1 := mkP t1 in constr:(@FEopp C e1)
         | (rdiv ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEdiv e1 e2)
+          let e2 := mkP t2 in constr:(@FEdiv C e1 e2)
         | (rinv ?t1) =>
-          fun _ => let e1 := mkP t1 in constr:(FEinv e1)
+          fun _ => let e1 := mkP t1 in constr:(@FEinv C e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant =>
             fun _ =>
             let p := Find_at t fv in
             constr:(@FEX C p)
-          | ?c => fun _ => let e1 := mkP t1 in constr:(FEpow e1 c)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(@FEpow C e1 c)
           end
         | _ =>
           fun _ =>
           let p := Find_at t fv in
           constr:(@FEX C p)
         end
-    | ?c => fun _ => constr:(FEc c)
+    | ?c => fun _ => constr:(@FEc C c)
     end in
     f ()
  in mkP t.