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/field/closed_field.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 24b764b..4ee11f3 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -194,6 +194,7 @@ Proof. by move=> a n; elim: n a=> [a /= -> //|n ihn a ra]; apply: ihn. Qed.
 Fixpoint sumpT (p q : polyF) :=
   match p, q with a :: p, b :: q => (a + b)%T :: sumpT p q
                 | [::], q => q | p, [::] => p end.
+Arguments sumpT : simpl nomatch.
 
 Lemma eval_sumpT (p q : polyF) (e : seq F) :
   eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).
-- 
cgit v1.2.3