search

coq-community / coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Other
65 stars 17 forks source link

Unnecessary assumption in sorted_take #40

Open ybertot opened 3 years ago

ybertot commented 3 years ago

Hello, in CoqEAL0.1, sorted_take (from ssrcomplements.v) had no transitivity assumption. In CoqEAL1.0.5, such an assumption exists. It may turn out be a problem one day.

proux01 commented 3 years ago

Indeed, this lemma should be removed as it is now in MC https://github.com/math-comp/math-comp/blob/14097e37cb3b0590ef5d91809acf4fed0fb22f1a/mathcomp/ssreflect/path.v#L369

ybertot commented 3 years ago

I do not understand. sorted_take does not occur in the current master branch of math-comp. What is the commit that @proux01 mentions attached to?

proux01 commented 3 years ago

It's take_sorted : https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/path.v#L369

ybertot commented 3 years ago

thks, I did not pay enough attention.

proux01 commented 3 years ago

I'd rather keep this open to remember to do the change once MC 1.13 is out.