From 1432318faa4cb6a50eca2c7a371b43b3b9969666 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Fri, 25 Apr 2014 16:17:15 +0200 Subject: Pos.iter arguments in a better order for cbn. --- theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 5aa31d7bd..03fc58c55 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -2232,7 +2232,7 @@ Section Int31_Specs. 2: simpl; unfold Z.pow_pos; simpl; auto with zarith. case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4. unfold base, Z.pow, Z.pow_pos in H2,H4; simpl in H2,H4. - unfold phi2,Z.pow, Z.pow_pos. simpl Pos.iter; auto with zarith. } + unfold phi2. cbn [Z.pow Z.pow_pos Pos.iter]. auto with zarith. } case (iter312_sqrt_correct 31 (fun _ _ j => j) ih il Tn); auto with zarith. change [|Tn|] with 2147483647; auto with zarith. intros j1 _ HH; contradict HH. -- cgit v1.2.3