diff options
| author | Jason Gross <jasongross9@gmail.com> | 2018-01-17 15:40:12 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-01-17 15:40:12 +0100 |
| commit | 7d3440a69c3a344613b11e7fe4b5f20a655d177f (patch) | |
| tree | 4359ce9940bb77d3e92b0677c09b5645d0a252cd /flocq | |
| parent | 51a10cf84b2d762b9f83b7387c022294423b3b78 (diff) | |
| download | compcert-kvx-7d3440a69c3a344613b11e7fe4b5f20a655d177f.tar.gz compcert-kvx-7d3440a69c3a344613b11e7fe4b5f20a655d177f.zip | |
Don't depend on the judgmental behavior of Bool.eqb (#217)
This change is backwards compatible, and makes flocq compatible with
https://github.com/coq/coq/pull/6596. Was applied to the Flocq master sources
https://gitlab.inria.fr/flocq/flocq/commit/db356aa5ea0fd0234e3872f70e8972086055cd57
Diffstat (limited to 'flocq')
| -rw-r--r-- | flocq/Appli/Fappli_rnd_odd.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v index b6d985ac..273c1000 100644 --- a/flocq/Appli/Fappli_rnd_odd.v +++ b/flocq/Appli/Fappli_rnd_odd.v @@ -199,7 +199,7 @@ case (Zeven (Zfloor r)); simpl; ring. apply trans_eq with (Zeven (Zceil r)). rewrite Zceil_floor_neq. rewrite Zeven_plus. -simpl; reflexivity. +destruct (Zeven (Zfloor r)); reflexivity. now apply sym_not_eq. rewrite <- (Zeven_opp (Zfloor (- r))). reflexivity. |