diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2019-05-06 20:12:45 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-06 20:12:45 +0200 |
| commit | e9c136508ee6e51f26d280ac17370d724b05bf41 (patch) | |
| tree | d27de5dfeb89adf3802dbc74841628799dd443b0 /flocq/Prop/Relative.v | |
| parent | 8df51b9866ccda99980e9f4de7ec2f2a0cd416e6 (diff) | |
| download | compcert-kvx-e9c136508ee6e51f26d280ac17370d724b05bf41.tar.gz compcert-kvx-e9c136508ee6e51f26d280ac17370d724b05bf41.zip | |
Make scripts compatible with new behavior of field_simplify (#291)
The `field_simplify` tactics will be improved soon (https://github.com/coq/coq/pull/9854).
Flocq was made compatible with this improvement (https://gitlab.inria.fr/flocq/flocq/commit/0752761a6a344d62f6bc728eac442ebb4ba655ac).
This commit updates CompCert's copy of Flocq accordingly.
Diffstat (limited to 'flocq/Prop/Relative.v')
| -rw-r--r-- | flocq/Prop/Relative.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Prop/Relative.v b/flocq/Prop/Relative.v index b936f2f7..5f87bd84 100644 --- a/flocq/Prop/Relative.v +++ b/flocq/Prop/Relative.v @@ -566,7 +566,7 @@ assert (H : (Rabs ((rx - x) / x) <= u_ro / (1 + u_ro))%R). now rewrite (Rabs_Rinv _ Nzx); apply Rinv_le. } apply (Rmult_le_reg_r ((ufpx + Rabs (rx - x)) * (1 + u_ro))). { apply Rmult_lt_0_compat; lra. } - field_simplify; [unfold Rdiv; rewrite Rinv_1, !Rmult_1_r| |]; lra. } + field_simplify; [try unfold Rdiv; rewrite ?Rinv_1, ?Rmult_1_r| |]; lra. } revert H; unfold Rdiv; rewrite Rabs_mult, (Rabs_Rinv _ Nzx); intro H. apply (Rmult_le_reg_r (/ Rabs x)); [now apply Rinv_0_lt_compat, Rabs_pos_lt|]. now apply (Rle_trans _ _ _ H); right; field; split; [apply Rabs_no_R0|lra]. |