diff options
| author | Cyril Cohen | 2020-11-20 02:31:40 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-20 20:50:44 +0100 |
| commit | c55acd1fefa970cc4ed3a8a53b05fd77008a7cdf (patch) | |
| tree | 864b98bd44a865c6155e96746a4c837061a51888 /mathcomp/field/closed_field.v | |
| parent | fd0d84084738decce3fb6557cf82dc10d030daa8 (diff) | |
Tuning simplifications using Arguments simpl nomatch
Diffstat (limited to 'mathcomp/field/closed_field.v')
| -rw-r--r-- | mathcomp/field/closed_field.v | 1 |
1 files changed, 1 insertions, 0 deletions
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). |