Modularization of BinPos + fixes in Stdlib

 BinPos now contain a sub-module Pos, in which are placed functions
 like add (ex-Pplus), mul (ex-Pmult), ... and properties like
 add_comm, add_assoc, ...

 In addition to the name changes, the organisation is changed quite
 a lot, to try to take advantage more of the orders < and <= instead
 of speaking only of the comparison function.

 The main source of incompatibilities in scripts concerns this compare:
 Pos.compare is now a binary operation, expressed in terms of the
 ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
 this ternary version being called now Pos.compare_cont. As for everything
 else, compatibility notations (only parsing) are provided. But notations
 "_ ?= _" on positive will have to be edited, since they now point to
 Pos.compare.

 We also make the sub-module Pos to be directly an OrderedType,
 and include results about min and max.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 1acdd17e5..2dd1c3eec 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -2245,7 +2245,7 @@ Section Int31_Specs.
   2: simpl; unfold Zpower_pos; simpl; auto with zarith.
   case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4.
   unfold base, Zpower, Zpower_pos in H2,H4; simpl in H2,H4.
-  unfold phi2,Zpower, Zpower_pos; simpl iter_pos; auto with zarith.
+  unfold phi2,Zpower, Zpower_pos. simpl 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.