From c55acd1fefa970cc4ed3a8a53b05fd77008a7cdf Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 20 Nov 2020 02:31:40 +0100
Subject: Tuning simplifications using Arguments simpl nomatch

---
 mathcomp/ssreflect/binomial.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mathcomp/ssreflect/binomial.v')

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.
 
-- 
cgit v1.2.3