aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/binomial.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
-rw-r--r--mathcomp/ssreflect/binomial.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index cd3ec87..02d2e48 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -178,6 +178,7 @@ Fixpoint binomial_rec n m :=
| _, 0 => 1
| 0, _.+1 => 0
end.
+Arguments binomial_rec : simpl nomatch.
Definition binomial := nosimpl binomial_rec.