diff options
| author | Hugo Herbelin | 2014-08-17 18:20:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:39 +0200 |
| commit | e8a531dfa623e3badc3baddcf13f0a7975c37886 (patch) | |
| tree | bfd59d295e477975d8bd49024011ec8d265154ce /theories | |
| parent | 602544c70684794e34030757ff986eaa5b519069 (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.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 043b68dd3c..c658230d5f 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. |