diff options
| author | msozeau | 2008-04-28 09:27:17 +0000 |
|---|---|---|
| committer | msozeau | 2008-04-28 09:27:17 +0000 |
| commit | 3478ffda0a0a83951db341eb68fc6b71877c1392 (patch) | |
| tree | 7e4bc66924da99168e75bcc5b4e614190d68aa9b /theories/Ints | |
| parent | 7a4ccdc7eb1a6afd21768963a249ec3617584482 (diff) | |
Backtrack on using metas eagerly in auto, only done in "new auto" for
now. Fix proof scripts that failed correspondingly. Should make many
contribs compile again...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Ints')
| -rw-r--r-- | theories/Ints/num/NMake.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index c857da3857..8cb779350a 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -5182,6 +5182,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^1) with (2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_2; unfold to_Z. apply (znz_of_pos_correct w2_spec). @@ -5189,6 +5190,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^2) with (2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_3; unfold to_Z. apply (znz_of_pos_correct w3_spec). @@ -5196,6 +5198,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^3) with (2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_4; unfold to_Z. apply (znz_of_pos_correct w4_spec). @@ -5203,6 +5206,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^4) with (2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_5; unfold to_Z. apply (znz_of_pos_correct w5_spec). @@ -5210,6 +5214,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^5) with (2 * 2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_6; unfold to_Z. apply (znz_of_pos_correct w6_spec). @@ -5217,6 +5222,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^6) with (2 * 2 * 2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n. intros H1; rewrite spec_reduce_n; unfold to_Z. simpl minus; rewrite <- minus_n_O. |