From e8a531dfa623e3badc3baddcf13f0a7975c37886 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 17 Aug 2014 18:20:05 +0200 Subject: Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to integrate to "rewrite"?) with the code of "replace". Incidentally, "inversion" relies on dependent rewrite, with an incompatibility introduced. Left-to-right rewriting is now done with "eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The first one reduces to the second one but simpl is not anymore able to reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see Zdigits). --- theories/ZArith/Zdigits.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/ZArith') diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 043b68dd3..c658230d5 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -152,7 +152,7 @@ Section Z_BRIC_A_BRAC. Lemma binary_value_pos : forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z. Proof. - induction bv as [| a n v IHbv]; simpl. + induction bv as [| a n v IHbv]; cbn. omega. destruct a; destruct (binary_value n v); simpl; auto. -- cgit v1.2.3