| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-18 | Merge PR #6305: Build with windows line endings | Maxime Dénès | |
| 2017-12-18 | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | |
| 2017-12-18 | Merge PR #6453: [doc] Nit on the manual. | Maxime Dénès | |
| 2017-12-18 | Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording | Maxime Dénès | |
| 2017-12-18 | Merge PR #6419: [vernac] Split `command.ml` into separate files. | Maxime Dénès | |
| 2017-12-18 | Merge PR #6413: [econstr] Switch constrintern API to non-imperative style. | Maxime Dénès | |
| 2017-12-17 | [flags] Make program_mode a parameter for commands in vernac. | Emilio Jesus Gallego Arias | |
| This is useful as it allows to reflect program_mode behavior as an attribute. | |||
| 2017-12-17 | [vernac] Split `command.ml` into separate files. | Emilio Jesus Gallego Arias | |
| Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413. | |||
| 2017-12-17 | [doc] Nit on the manual. | Emilio Jesus Gallego Arias | |
| `ssrnat` is mentioned, but it is not distributed with Coq. | |||
| 2017-12-16 | Fix build file | Jim | |
| 2017-12-16 | For bug 6249, Segmentation fault when building Coq on Windows 10. | Jim | |
| Enable builds on Windows by removing Windows-style endings where it impacts make. The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here. | |||
| 2017-12-15 | Overlay for unimath. | Gaëtan Gilbert | |
| 2017-12-15 | Do dependencies in 1 command per file class. | Gaëtan Gilbert | |
| 2017-12-15 | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml` | Maxime Dénès | |
| 2017-12-15 | Merge PR #6431: Compatibility of the Coq macOS package with OS X 10.11. | Maxime Dénès | |
| 2017-12-15 | Merge PR #6219: Document undocumented options | Maxime Dénès | |
| 2017-12-15 | Merge PR #6429: 8.7.1 CHANGES. | Maxime Dénès | |
| 2017-12-15 | [econstr] Switch constrintern API to non-imperative style. | Emilio Jesus Gallego Arias | |
| We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there. | |||
| 2017-12-15 | Compatibility of the Coq macOS package with OS X 10.11. | Théo Zimmermann | |
| Travis has moved on to macOS 10.12 but this makes the package incompatible with earlier versions. This fix should restore the compatibility with OS X 10.11. | |||
| 2017-12-14 | Deprecate dead option Match Strict (ssr). | Gaëtan Gilbert | |
| 2017-12-14 | Deprecate dead code option Congruence Depth. | Gaëtan Gilbert | |
| 2017-12-14 | Merge PR #6386: Catch errors while coercing 'and' intro patterns | Maxime Dénès | |
| 2017-12-14 | Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match ↵ | Maxime Dénès | |
| (fix #6106) | |||
| 2017-12-14 | Merge PR #6379: Fix profiling plugin | Maxime Dénès | |
| 2017-12-14 | Merge PR #6422: [meta] Minor linking fix. | Maxime Dénès | |
| 2017-12-14 | Merge PR #6264: [kernel] Patch allowing to disable VM reduction. | Maxime Dénès | |
| 2017-12-14 | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵ | Maxime Dénès | |
| same right-hand side. | |||
| 2017-12-14 | Merge PR #6373: Further clean-up in Reductionops, removing unused lift ↵ | Maxime Dénès | |
| arguments. | |||
| 2017-12-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès | |
| 2017-12-14 | 8.7.1 CHANGES. | Théo Zimmermann | |
| 2017-12-14 | Document Short Module Printing. | Gaëtan Gilbert | |
| 2017-12-14 | Document Rewriting Schemes (quickly). | Gaëtan Gilbert | |
| 2017-12-14 | Document Record Elimination Schemes. | Gaëtan Gilbert | |
| 2017-12-14 | Document Asymmetric Patterns. | Gaëtan Gilbert | |
| 2017-12-14 | Document some omega options (missing Omega Oldstyle). | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug RAKAM. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Debug Cbv. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Info/Debug Auto/Trivial/Eauto. | Gaëtan Gilbert | |
| 2017-12-14 | Add optindex for Set Bullet Behavior. | Gaëtan Gilbert | |
| 2017-12-14 | Add doc for Set Congruence Verbose | Gaëtan Gilbert | |
| 2017-12-14 | Fix typo in doc optindex for Typeclass Resolution ... | Gaëtan Gilbert | |
| 2017-12-14 | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | Maxime Dénès | |
| 2017-12-14 | Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards ↵ | Maxime Dénès | |
| compatible change. | |||
| 2017-12-14 | Merge PR #6388: Fix issue #6387 | Maxime Dénès | |
| 2017-12-13 | Merge PR #1108: [stm] Reorganize flags | Maxime Dénès | |
| 2017-12-13 | Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check. | Maxime Dénès | |
| 2017-12-13 | Merge PR #6251: [proof] Embed evar_map in RefinerError exception. | Maxime Dénès | |
| 2017-12-13 | Merge PR #6175: Restoring filtering of native files passed to `rm` during ↵ | Maxime Dénès | |
| `make clean`. | |||
| 2017-12-13 | [meta] Minor linking fix. | Emilio Jesus Gallego Arias | |
| 2017-12-13 | [econstr] Small cleanup in `vernac/lemmas` | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |