diff options
Diffstat (limited to 'theories/PArith')
| -rw-r--r-- | theories/PArith/BinPos.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 0ffce766c..64e32c560 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Unset Boxed Definitions. - Declare ML Module "z_syntax_plugin". (**********************************************************************) @@ -65,8 +63,6 @@ Fixpoint Psucc (x:positive) : positive := (** ** Addition *) -Set Boxed Definitions. - Fixpoint Pplus (x y:positive) : positive := match x, y with | p~1, q~1 => (Pplus_carry p q)~0 @@ -93,8 +89,6 @@ with Pplus_carry (x y:positive) : positive := | 1, 1 => 1~1 end. -Unset Boxed Definitions. - Infix "+" := Pplus : positive_scope. Definition Piter_op {A}(op:A->A->A) := |