From 0d0e9738fa5ec96be85796e5cb8486de00018155 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 18 Aug 2016 16:27:59 +0200 Subject: Fix an occurrence of deprecated eqn syntax in stdlib. --- theories/Reals/Sqrt_reg.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Reals') diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 10527442e..d43baee8c 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -339,7 +339,7 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. rewrite Rabs_right. -- cgit v1.2.3