Imported Upstream version 8.6

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index fe38ea4f..850afe53 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