aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-08-17 18:20:05 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-08-18 18:56:39 +0200
commite8a531dfa623e3badc3baddcf13f0a7975c37886 (patch)
treebfd59d295e477975d8bd49024011ec8d265154ce /theories
parent602544c70684794e34030757ff986eaa5b519069 (diff)
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).
Diffstat (limited to 'theories')
-rw-r--r--theories/ZArith/Zdigits.v2
1 files changed, 1 insertions, 1 deletions
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.