diff options
| author | affeldt-aist | 2020-11-22 19:31:22 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-22 19:31:22 +0900 |
| commit | d954da5acab8c1ed0786f05766e2161b5c09bcca (patch) | |
| tree | 864b98bd44a865c6155e96746a4c837061a51888 /mathcomp/ssreflect/binomial.v | |
| parent | fd0d84084738decce3fb6557cf82dc10d030daa8 (diff) | |
| parent | c55acd1fefa970cc4ed3a8a53b05fd77008a7cdf (diff) | |
Merge pull request #661 from CohenCyril/tune_simplification
Tuning simplifications using Arguments nomatch
Diffstat (limited to 'mathcomp/ssreflect/binomial.v')
| -rw-r--r-- | mathcomp/ssreflect/binomial.v | 1 |
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. |