| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | canonical-structures.rst | 14005 | logplain |
| -rw-r--r-- | extended-pattern-matching.rst | 18846 | logplain |
| -rw-r--r-- | extraction.rst | 23470 | logplain |
| -rw-r--r-- | generalized-rewriting.rst | 35493 | logplain |
| -rw-r--r-- | implicit-coercions.rst | 15861 | logplain |
| -rw-r--r-- | micromega.rst | 10768 | logplain |
| -rw-r--r-- | miscellaneous-extensions.rst | 1836 | logplain |
| -rw-r--r-- | nsatz.rst | 3933 | logplain |
| -rw-r--r-- | omega.rst | 5765 | logplain |
| -rw-r--r-- | parallel-proof-processing.rst | 10621 | logplain |
| -rw-r--r-- | program.rst | 13310 | logplain |
| -rw-r--r-- | ring.rst | 29123 | logplain |
| -rw-r--r-- | type-classes.rst | 20308 | logplain |
| -rw-r--r-- | universe-polymorphism.rst | 15094 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |