diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-08-18 16:27:59 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-08-18 16:27:59 +0200 |
| commit | 0d0e9738fa5ec96be85796e5cb8486de00018155 (patch) | |
| tree | c689affbabf6565e16ec5d8b415be3ab7815af3f /theories/Reals | |
| parent | ce9058b597fc53310619d537aadacc091755ed39 (diff) | |
Fix an occurrence of deprecated eqn syntax in stdlib.
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Sqrt_reg.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |