| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-02-25 | Merge PR #13202: Infrastructure for fine-grained debug flags | coqbot-app[bot] | |
| Reviewed-by: gares Ack-by: herbelin Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer Ack-by: ejgallego | |||
| 2021-02-24 | Infrastructure for fine-grained debug flags | Maxime Dénès | |
| 2021-02-16 | Get rid of the compilation date from the binaries to make them more stable. | Guillaume Melquiond | |
| Contrarily to the comments, Coq_config.date was not the "release date" but just another "compile date". | |||
| 2021-02-10 | Merge PR #13821: Properly handle ordering of -w and -native-compiler | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2021-02-04 | Remove deprecated -inputstate command line argument | Gaëtan Gilbert | |
| Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014) | |||
| 2021-02-04 | Remove deprecated -sprop-cumulative command line argument | Gaëtan Gilbert | |
| Deprecated since #12034 (8.12) | |||
| 2021-02-04 | Properly handle ordering of -w and -native-compiler | Gaëtan Gilbert | |
| Warnings are handled as injection commands, interleaved with options and requires. Native compiler impacts require, so we must convert "yes" to "no" before handling injections. As such the semantic handling of the native command line argument must be separated from the emission of the warning message, which this PR implements. Fix #13819 In principle the other 2 cwarning in coqargs (deprecated spropcumul and inputstate) should be moved to injections too, but since they're deprecated I can't be bothered. | |||
| 2021-01-27 | make the linter happy | Enrico Tassi | |
| 2021-01-27 | [coqargs] use standard option injection for -print-emacs | Enrico Tassi | |
| 2021-01-27 | [coqargs] use standard option injection for -type-in-type | Enrico Tassi | |
| 2021-01-27 | [coqargs] use standard option injection for -mangle-names | Enrico Tassi | |
| 2021-01-27 | [coqtop] handle -print-module-uid after initialization | Enrico Tassi | |
| 2021-01-27 | [coqc] move -output-context from sysinit/coqargs to coqc proper | Enrico Tassi | |
| 2021-01-27 | [sysinit] move initialization code from coqtop to here | Enrico Tassi | |
| We also spill (some) non-generic arguments and initialization code out of coqargs and to coqtop, namely colors for the terminal. There are more of these, left to later commits. | |||
| 2021-01-27 | [sysinit] new component for system initialization | Enrico Tassi | |
| This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |