index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-04-08
Merge pull request #324 from math-comp/seq-permutations-allpairs
Cyril Cohen
2019-04-08
New test cases generation: corrent implementation of least common children
Kazuhiko Sakaguchi
2019-04-06
Permutations and other extensions to seq; fintype documentation
Georges Gonthier
2019-04-06
Fix inheritance bugs in finalg and extremal
Kazuhiko Sakaguchi
2019-04-05
least common childen
Cyril Cohen
2019-04-04
no output on success in test_suite/hierarchy_test.v (#323)
Cyril Cohen
2019-04-04
porting ChangeLog to Markdown format (#322)
Enrico
2019-04-04
Merge pull request #321 from math-comp/remove-8.6
Cyril Cohen
2019-04-04
remove support for Coq 8.6
Enrico Tassi
2019-04-04
Merge pull request #320 from math-comp/fix-test-suite
Enrico
2019-04-03
rename test-suite -> test_suite to make coq happy
Enrico Tassi
2019-04-03
Merge pull request #291 from pi8027/finalg-hierarchy
Cyril Cohen
2019-04-03
Fix inheritances in ssrnum
Kazuhiko Sakaguchi
2019-04-02
Fix inheritances in countalg and finalg (the 2nd attempt)
Kazuhiko Sakaguchi
2019-04-02
speedup in hierarchy_test.py
Cyril Cohen
2019-04-02
identifying missing joins
Cyril Cohen
2019-04-01
Merge pull request #294 from math-comp/dependent-positive-finfun
Cyril Cohen
2019-04-01
ChangeLog update
Georges Gonthier
2019-04-01
locking definitions to address `integral.v` divergence
Georges Gonthier
2019-04-01
Compatibility fix for Coq issue coq/#9663
Georges Gonthier
2019-04-01
Expand sample use as container in Inductive
Georges Gonthier
2019-04-01
Making {fun ...} structural and extending it to dependent functions
Georges Gonthier
2019-04-01
Improve CI head tracking
Georges Gonthier
2019-03-29
Merge pull request #292 from erikmd/under-support
Cyril Cohen
2019-03-26
Merge pull request #304 from CohenCyril/allsigs
Cyril Cohen
2019-03-26
Refactoring allpairs to handle the dependent version as well
Cyril Cohen
2019-03-26
Merge pull request #305 from CohenCyril/sumn
Cyril Cohen
2019-03-26
Merge pull request #301 from CohenCyril/mem_remF
Enrico
2019-03-24
Compat of sumn with bigop and renaming dep to cond when appropriate
Cyril Cohen
2019-03-22
missing lemma in seq.v
Cyril Cohen
2019-03-22
Merge pull request #303 from CohenCyril/ffun0
Assia Mahboubi
2019-03-21
adding ffun0
Cyril Cohen
2019-03-20
Add extra eta lemmas for the under tactic
Erik Martin-Dorel
2019-03-20
Merge pull request #300 from erikmd/doc-detail
Cyril Cohen
2019-03-20
[doc] Mention that fingraph's connect computes the reflexive transitive closure
Erik Martin-Dorel
2019-03-19
Fix countalg to finalg inheritances
Kazuhiko Sakaguchi
2019-03-19
Merge pull request #290 from pi8027/hierarchy-diagram
Cyril Cohen
2019-03-18
Merge pull request #298 from math-comp/fix-hidden-branch-types
Georges Gonthier
2019-03-18
remove dependency on hidden case branch types
Georges Gonthier
2019-03-14
Merge pull request #295 from pi8027/export-addrKA-subrKA
Cyril Cohen
2019-03-07
Put documentation and some command line options for hierarchy-diagram
Kazuhiko Sakaguchi
2019-03-07
Use both coercions and canonical projections to generate the diagram
Kazuhiko Sakaguchi
2019-03-05
Export addrKA and subrKA from GRing.Theory
Kazuhiko Sakaguchi
2019-02-22
Reimplement hierarchy-diagram by using coercions between "<module>.type" types
Kazuhiko Sakaguchi
2019-02-22
Add a tool to draw the hierarchy diagram
Kazuhiko Sakaguchi
2019-02-07
pmap_cat, pmap_perm and perm_map_inj added (#277)
Søren Eller Thomsen
2019-02-07
add a link to the website (#274)
Enrico
2019-02-07
Add the eqType instance for intervals, le_bound(l|r)_anti, and itv_intersecti...
Kazuhiko Sakaguchi
2019-02-05
we silence warnings that just pollute our logs (#275)
Enrico
2019-02-05
fix etc/utils/packager (#273)
Cyril Cohen
[prev]
[next]