| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | 00000-title.rst | 14 | logplain |
| -rw-r--r-- | 11906-micromega-booleans.rst | 260 | logplain |
| -rw-r--r-- | 12399-rm-prolog.rst | 159 | logplain |
| -rw-r--r-- | 12423-rm-info.rst | 133 | logplain |
| -rw-r--r-- | 12552-zify-pre-hook.rst | 182 | logplain |
| -rw-r--r-- | 12816-master+fix12787-K-redex-injection-anomaly.rst | 244 | logplain |
| -rw-r--r-- | 12847-master+inversion-works-with-eq-in-type.rst | 299 | logplain |
| -rw-r--r-- | 12993-remove-cutrewrite.rst | 157 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |