| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | canonical-structures.rst | 110 | logplain |
| -rw-r--r-- | extended-pattern-matching.rst | 106 | logplain |
| -rw-r--r-- | extraction.rst | 26840 | logplain |
| -rw-r--r-- | generalized-rewriting.rst | 38929 | logplain |
| -rw-r--r-- | implicit-coercions.rst | 14391 | logplain |
| -rw-r--r-- | micromega.rst | 13692 | logplain |
| -rw-r--r-- | miscellaneous-extensions.rst | 1816 | logplain |
| -rw-r--r-- | nsatz.rst | 4377 | logplain |
| -rw-r--r-- | parallel-proof-processing.rst | 11044 | logplain |
| -rw-r--r-- | program.rst | 13062 | logplain |
| -rw-r--r-- | ring.rst | 30100 | logplain |
| -rw-r--r-- | sprop.rst | 9674 | logplain |
| -rw-r--r-- | type-classes.rst | 23758 | logplain |
| -rw-r--r-- | universe-polymorphism.rst | 22495 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |