diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-03 15:21:05 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-03 15:21:05 +0000 |
| commit | 66ee4884f2c301eeac1f73deb97d6b50d1faa8bd (patch) | |
| tree | 2a560e56d366ef92c86985595e5e1f708b6b3243 /theories/QArith | |
| parent | 6832c60f741e6bfb2a850d567fd6a1dff7059393 (diff) | |
(Try to) use the conversion oracle also in w_unify to choose which constant to
unfold first. The patch changes the usual order of unifications so some
may differ (only one example in the stdlib breaks because of more
unification happening).
Actually this change was trigerred because of an incompleteness which is
not resolved here. At least this way unfolding is consistent between
w_unify and the kernel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/Qpower.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 8672592d9..efaefbb7c 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -221,7 +221,7 @@ repeat rewrite Zpos_mult_morphism. repeat rewrite Z2P_correct. repeat rewrite Zpower_pos_1_r; ring. apply Zpower_pos_pos; red; auto. -repeat apply Zmult_lt_0_compat; auto; +repeat apply Zmult_lt_0_compat; red; auto; apply Zpower_pos_pos; red; auto. (* xO *) rewrite IHp, <-Pplus_diag. |