From 62b8190fd4b1c2223eb0a89329a28ca66d11a326 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 17 Oct 2014 15:40:49 +0200 Subject: Revert "Essai où assert_style n'est utilisé que si pas visuellement une équation;" which was committed by mistake. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee. --- theories/QArith/Qreduction.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/QArith') diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 7d8ed5275..2aac617eb 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -46,12 +46,12 @@ Proof. generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). - simpl. intros <- Hg1 Hg2 (Hg3,Hg4). clear H0. - assert (Hg0 : g <> 0). (intro; now subst g). Show Proof. + simpl. intros <- Hg1 Hg2 (Hg3,Hg4). + assert (Hg0 : g <> 0) by (intro; now subst g). generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)). destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). - simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). clear H0. + simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). assert (Hg'0 : g' <> 0) by (intro; now subst g'). elim (rel_prime_cross_prod aa bb cc dd). -- cgit v1.2.3