diff options
Diffstat (limited to 'plugins/setoid_ring/Cring.v')
-rw-r--r-- | plugins/setoid_ring/Cring.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 02194d4f1..cb2e78e42 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -21,6 +21,7 @@ Require Export Ncring_tac. Class Cring {R:Type}`{Rr:Ring R} := cring_mul_comm: forall x y:R, x * y == y * x. + Ltac reify_goal lvar lexpr lterm:= (*idtac lvar; idtac lexpr; idtac lterm;*) match lexpr with @@ -30,10 +31,10 @@ Ltac reify_goal lvar lexpr lterm:= |- (?op ?u1 ?u2) => change (op (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e1) (@Ring_polynom.PEeval - _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) + _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e2)) end end. |