From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 theories/Numbers/Integer/Abstract/ZDivEucl.v  | 2 +-
 theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +-
 theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d0df8fb4a7..ab73ebfe1d 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -391,7 +391,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, 0<b -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index d5f3f4ada7..c8260e516f 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -436,7 +436,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, 0<b -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index de2e99ec3a..464fe354b8 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -404,7 +404,7 @@ Proof.
 intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto.
 Qed.
 
-(** Some additionnal inequalities about quot. *)
+(** Some additional inequalities about quot. *)
 
 Theorem quot_lt_upper_bound:
   forall a b q, 0<=a -> 0<b -> a < b*q -> a÷b < q.
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 theories/Numbers/Integer/Abstract/ZAdd.v        | 2 +-
 theories/Numbers/Integer/Abstract/ZAddOrder.v   | 2 +-
 theories/Numbers/Integer/Abstract/ZAxioms.v     | 2 +-
 theories/Numbers/Integer/Abstract/ZBase.v       | 2 +-
 theories/Numbers/Integer/Abstract/ZBits.v       | 2 +-
 theories/Numbers/Integer/Abstract/ZDivEucl.v    | 2 +-
 theories/Numbers/Integer/Abstract/ZDivFloor.v   | 2 +-
 theories/Numbers/Integer/Abstract/ZDivTrunc.v   | 2 +-
 theories/Numbers/Integer/Abstract/ZGcd.v        | 2 +-
 theories/Numbers/Integer/Abstract/ZLcm.v        | 2 +-
 theories/Numbers/Integer/Abstract/ZLt.v         | 2 +-
 theories/Numbers/Integer/Abstract/ZMaxMin.v     | 2 +-
 theories/Numbers/Integer/Abstract/ZMul.v        | 2 +-
 theories/Numbers/Integer/Abstract/ZMulOrder.v   | 2 +-
 theories/Numbers/Integer/Abstract/ZParity.v     | 2 +-
 theories/Numbers/Integer/Abstract/ZPow.v        | 2 +-
 theories/Numbers/Integer/Abstract/ZProperties.v | 2 +-
 theories/Numbers/Integer/Abstract/ZSgnAbs.v     | 2 +-
 theories/Numbers/Integer/BigZ/BigZ.v            | 2 +-
 theories/Numbers/Integer/BigZ/ZMake.v           | 2 +-
 theories/Numbers/Integer/Binary/ZBinary.v       | 2 +-
 theories/Numbers/Integer/NatPairs/ZNatPairs.v   | 2 +-
 theories/Numbers/Integer/SpecViaZ/ZSig.v        | 2 +-
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 +-
 24 files changed, 24 insertions(+), 24 deletions(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index ec8801c4e8..f7fdc17950 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index e341ea8a56..6bf5e9d4c5 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 2a9fa539a0..ad10e65f00 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 6634eab1df..9b1b30f878 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 9dd0ec0ee1..c919e121db 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index ab73ebfe1d..278e1bcffa 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index c8260e516f..310748ddb3 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 464fe354b8..0430107792 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
index cf6ff79ecd..30adaeb4b1 100644
--- a/theories/Numbers/Integer/Abstract/ZGcd.v
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
index 9a1768eb17..ef33308c28 100644
--- a/theories/Numbers/Integer/Abstract/ZLcm.v
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 6d0cdb0191..0c92918d13 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v
index 07c78ead3f..24a47f002f 100644
--- a/theories/Numbers/Integer/Abstract/ZMaxMin.v
+++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 2d78d8f30c..830c0a7da0 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 487aaae1c8..320c8f355a 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
index 195a0277ed..952d8e9c12 100644
--- a/theories/Numbers/Integer/Abstract/ZParity.v
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 87de2c782d..02b8501c79 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 5cfeeb2164..1dec3c5869 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
index b379853edc..a10552ab3b 100644
--- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v
+++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index b28bc40f8e..ec495d0947 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index af4f1d9370..8673b8a58f 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 042081066e..eae8204d41 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 02f02fbc51..0aaf336576 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 30ac32b532..a360327a48 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index c9dc687cbf..32410d1d0b 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3


From d5656a6c28f79d59590d4fde60c5158a649d1b65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Mar 2016 11:16:03 +0100
Subject: Making parentheses mandatory in tactic scopes.

---
 theories/Numbers/Integer/BigZ/BigZ.v | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index ec495d0947..56cb9bbc2c 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -148,26 +148,26 @@ Ltac isBigZcst t :=
  match t with
  | BigZ.Pos ?t => isBigNcst t
  | BigZ.Neg ?t => isBigNcst t
- | BigZ.zero => constr:true
- | BigZ.one => constr:true
- | BigZ.two => constr:true
- | BigZ.minus_one => constr:true
- | _ => constr:false
+ | BigZ.zero => constr:(true)
+ | BigZ.one => constr:(true)
+ | BigZ.two => constr:(true)
+ | BigZ.minus_one => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigZcst t :=
  match isBigZcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Ltac BigZ_to_N t :=
  match t with
  | BigZ.Pos ?t => BigN_to_N t
- | BigZ.zero => constr:0%N
- | BigZ.one => constr:1%N
- | BigZ.two => constr:2%N
- | _ => constr:NotConstant
+ | BigZ.zero => constr:(0%N)
+ | BigZ.one => constr:(1%N)
+ | BigZ.two => constr:(2%N)
+ | _ => constr:(NotConstant)
  end.
 
 (** Registration for the "ring" tactic *)
-- 
cgit v1.2.3