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/ssreflect/prime.v | |
| parent | fd0d84084738decce3fb6557cf82dc10d030daa8 (diff) | |
Tuning simplifications using Arguments simpl nomatch
Diffstat (limited to 'mathcomp/ssreflect/prime.v')
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index ab8edce..ee5b136 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -76,6 +76,7 @@ Fixpoint elogn2 e q r {struct q} := | q'.+1, 1 => elogn2 e.+1 q' q' | q'.+1, r'.+2 => elogn2 e q' r' end. +Arguments elogn2 : simpl nomatch. Variant elogn2_spec n : nat * nat -> Type := Elogn2Spec e m of n = 2 ^ e * m.*2.+1 : elogn2_spec n (e, m). |