| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | 00000-title.rst | 18 | logplain |
| -rw-r--r-- | 13469-no-int-in-fail.rst | 222 | logplain |
| -rw-r--r-- | 13509-master+remove-bracketing-last-introduction-pattern-flag.rst | 246 | logplain |
| -rw-r--r-- | 13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst | 262 | logplain |
| -rw-r--r-- | 13568-master+fix13566-check-invalid-occurrences-especially-rewrite.rst | 280 | logplain |
| -rw-r--r-- | 13696-deprecate_at_in_conversion.rst | 282 | logplain |
| -rw-r--r-- | 13699-fix13579.rst | 253 | logplain |
| -rw-r--r-- | 13715-lia_implb.rst | 145 | logplain |
| -rw-r--r-- | 13741-remove_omega.rst | 391 | logplain |
| -rw-r--r-- | 13761-remove_convert_concl_nc.rst | 150 | logplain |
| -rw-r--r-- | 13762-remove_double_induction.rst | 465 | logplain |
| -rw-r--r-- | 13781-deprecate_micromega_options.rst | 169 | logplain |
| -rw-r--r-- | 13882-fix-ssr-setoidrw-in-hyp.rst | 414 | logplain |
| -rw-r--r-- | 14033-fix-14009.rst | 278 | logplain |
| -rw-r--r-- | 14089-ltac2_unify.rst | 184 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |