From 476d70df227f6880e7fce29c30f2158f83ce05b9 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 19 Jul 2012 14:59:28 +0000 Subject: Getting rid of the undocumented [complete] tactic, which was redundant with [solve]. The AST node still exists in Ltac, because this is used by the [assert ... by ...] tactical. Fixes #2847. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15625 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/setoid_ring/Field_theory.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/setoid_ring/Field_theory.v') diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index bd9622e52..0bd806c15 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -201,7 +201,7 @@ Theorem rdiv2: r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4). Proof. intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * r4); trivial. rewrite rdiv_simpl; trivial. rewrite (ARdistr_r Rsth Reqe ARth). @@ -223,7 +223,7 @@ assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring). assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring). assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring). assert (HH4: ~ r2 * (r4 * r5) == 0) - by complete (repeat apply field_is_integral_domain; trivial). + by (repeat apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * (r4 * r5)); trivial. rewrite rdiv_simpl; trivial. rewrite (ARdistr_r Rsth Reqe ARth). @@ -295,7 +295,7 @@ Hint Resolve rdiv6 . (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4). Proof. intros r1 r2 r3 r4 H H0. -assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial). +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). apply rmul_reg_l with (r2 * r4); trivial. rewrite rdiv_simpl; trivial. transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ]. -- cgit v1.2.3