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

---
 theories/Numbers/Cyclic/Int31/Ring31.v | 20 ++++++++++----------
 theories/Numbers/Integer/BigZ/BigZ.v   | 22 +++++++++++-----------
 theories/Numbers/Natural/BigN/BigN.v   | 24 ++++++++++++------------
 theories/Numbers/Rational/BigQ/BigQ.v  | 14 +++++++-------
 4 files changed, 40 insertions(+), 40 deletions(-)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index 215b8bd58..d160f5f1d 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -19,13 +19,13 @@ Local Open Scope list_scope.
 
 Ltac isInt31cst_lst l :=
  match l with
- | nil => constr:true
+ | nil => constr:(true)
  | ?t::?l => match t with
                | D1 => isInt31cst_lst l
                | D0 => isInt31cst_lst l
-               | _ => constr:false
+               | _ => constr:(false)
              end
- | _ => constr:false
+ | _ => constr:(false)
  end.
 
 Ltac isInt31cst t :=
@@ -38,17 +38,17 @@ Ltac isInt31cst t :=
       ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
       ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
     in isInt31cst_lst l
- | Int31.On => constr:true
- | Int31.In => constr:true
- | Int31.Tn => constr:true
- | Int31.Twon => constr:true
- | _ => constr:false
+ | Int31.On => constr:(true)
+ | Int31.In => constr:(true)
+ | Int31.Tn => constr:(true)
+ | Int31.Twon => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac Int31cst t :=
  match isInt31cst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 (** The generic ring structure inferred from the Cyclic structure *)
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index ec495d094..56cb9bbc2 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 *)
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 29a1145e0..ec1017f50 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -119,10 +119,10 @@ Qed.
 
 Ltac isStaticWordCst t :=
  match t with
- | W0 => constr:true
+ | W0 => constr:(true)
  | WW ?t1 ?t2 =>
    match isStaticWordCst t1 with
-   | false => constr:false
+   | false => constr:(false)
    | true => isStaticWordCst t2
    end
  | _ => isInt31cst t
@@ -139,30 +139,30 @@ Ltac isBigNcst t :=
  | BigN.N6 ?t => isStaticWordCst t
  | BigN.Nn ?n ?t => match isnatcst n with
    | true => isStaticWordCst t
-   | false => constr:false
+   | false => constr:(false)
    end
- | BigN.zero => constr:true
- | BigN.one => constr:true
- | BigN.two => constr:true
- | _ => constr:false
+ | BigN.zero => constr:(true)
+ | BigN.one => constr:(true)
+ | BigN.two => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigNcst t :=
  match isBigNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Ltac BigN_to_N t :=
  match isBigNcst t with
  | true => eval vm_compute in (BigN.to_N t)
- | false => constr:NotConstant
+ | false => constr:(NotConstant)
  end.
 
 Ltac Ncst t :=
  match isNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 (** Registration for the "ring" tactic *)
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index fe38ea4f2..850afe534 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -104,18 +104,18 @@ Ltac isBigQcst t :=
  | BigQ.Qz ?t => isBigZcst t
  | BigQ.Qq ?n ?d => match isBigZcst n with
              | true => isBigNcst d
-             | false => constr:false
+             | false => constr:(false)
              end
- | BigQ.zero => constr:true
- | BigQ.one => constr:true
- | BigQ.minus_one => constr:true
- | _ => constr:false
+ | BigQ.zero => constr:(true)
+ | BigQ.one => constr:(true)
+ | BigQ.minus_one => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigQcst t :=
  match isBigQcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Add Field BigQfield : BigQfieldth
-- 
cgit v1.2.3