From 7d3440a69c3a344613b11e7fe4b5f20a655d177f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 17 Jan 2018 15:40:12 +0100 Subject: 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 --- flocq/Appli/Fappli_rnd_odd.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'flocq') 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. -- cgit