diff options
Diffstat (limited to 'plugins/setoid_ring/Cring.v')
| -rw-r--r-- | plugins/setoid_ring/Cring.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index f13f509a..4872c776 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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. |