From 66ee4884f2c301eeac1f73deb97d6b50d1faa8bd Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 3 Oct 2008 15:21:05 +0000 Subject: (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 --- theories/QArith/Qpower.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories') 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. -- cgit v1.2.3