| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | 12218-proux01-numeral-notations-non-inductive.sh | 650 | logplain |
| -rw-r--r-- | 12449-SkySkimmer-minim-prop-toset.sh | 172 | logplain |
| -rw-r--r-- | 13075-ppedrot-explicit-names-quotient.sh | 306 | logplain |
| -rw-r--r-- | 13128-SkySkimmer-noinstance.sh | 149 | logplain |
| -rw-r--r-- | 13139-ppedrot-clean-hint-constr.sh | 295 | logplain |
| -rw-r--r-- | 13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh | 243 | logplain |
| -rw-r--r-- | README.md | 1599 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |