aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/discrete
ModeNameSize
l---------AUTHORS17logplain
l---------CeCILL-B18logplain
l---------INSTALL17logplain
-rw-r--r--Make145logplain
-rw-r--r--Makefile663logplain
l---------README16logplain
-rw-r--r--all.v283logplain
-rw-r--r--bigop.v73444logplain
-rw-r--r--binomial.v22866logplain
-rw-r--r--choice.v27668logplain
-rw-r--r--div.v34475logplain
-rw-r--r--finfun.v12096logplain
-rw-r--r--fingraph.v26743logplain
-rw-r--r--finset.v84916logplain
-rw-r--r--fintype.v76467logplain
-rw-r--r--generic_quotient.v27642logplain
-rw-r--r--opam466logplain
-rw-r--r--path.v33927logplain
-rw-r--r--prime.v57180logplain
-rw-r--r--tuple.v14879logplain