From af533645b1033dc386d8ac99cc8c4b6491b0ca91 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 29 Apr 2014 17:30:29 +0200 Subject: Fix Field_tac to get fast reification again, with the fix on template universe polymorphic constructors. --- plugins/setoid_ring/Field_tac.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins/setoid_ring/Field_tac.v') 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. -- cgit v1.2.3