summaryrefslogtreecommitdiff
path: root/theories/Numbers/Rational/BigQ/BigQ.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Rational/BigQ/BigQ.v')
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v14
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