| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | 00000-title.rst | 16 | logplain |
| -rw-r--r-- | 11986-float-low-level-printing.rst | 236 | logplain |
| -rw-r--r-- | 12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst | 198 | logplain |
| -rw-r--r-- | 12218-numeral-notations-non-inductive.rst | 936 | logplain |
| -rw-r--r-- | 12685-master+propagate-scope-in-indirect-applied-ref.rst | 326 | logplain |
| -rw-r--r-- | 12765-master+partial-app-in-recursive-notation.rst | 171 | logplain |
| -rw-r--r-- | 12950-master+reorganization-notations-only-parsing-only-printing.rst | 494 | logplain |
| -rw-r--r-- | 12960-master+fix9403-missing-flattening-app-notations.rst | 380 | logplain |
| -rw-r--r-- | 12965-master+fix9569-propagage-binding-vars-notations.rst | 244 | logplain |
| -rw-r--r-- | 12979-doc-numbers.rst | 178 | logplain |
| -rw-r--r-- | 12984-master+import-notation-make-active-again.rst | 638 | logplain |
| -rw-r--r-- | 12986-master+ordering-notation-by-precision.rst | 210 | logplain |
| -rw-r--r-- | 13092-master+fix-13078-no-binder-in-pattern-notation.rst | 208 | logplain |
| -rw-r--r-- | 13265-master+allow-single-binder-entry.rst | 271 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |