| 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-25 | Merge PR #13863: Get rid of the compilation date from the binaries to make ↵ | coqbot-app[bot] | |
| them more stable. Reviewed-by: SkySkimmer Reviewed-by: gares | |||
| 2021-02-24 | Infrastructure for fine-grained debug flags | Maxime Dénès | |
| 2021-02-17 | Add option --version to Coqide (fix #13752). | Guillaume Melquiond | |
| 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-02 | ide: lablgtk fixes | slrnsc | |
| 2021-02-01 | ide: shift+enter to find backwards | slrnsc | |
| 2021-01-28 | Merge PR #13763: Remove the SearchHead command (deprecated in 8.12) | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-27 | [coqtop] handle -print-module-uid after initialization | 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 | |||
| 2021-01-25 | Remove the SearchHead command | Jim Fehrle | |
| 2021-01-13 | Avoid using "subgoals" in the UI, it means the same as "goals" | Jim Fehrle | |
| 2020-12-18 | Fixes #13657: vscoq needs goal uid. | Hugo Herbelin | |
| 2020-10-30 | Adding support for printing goal names in CoqIDE. | Hugo Herbelin | |
| Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | |||
| 2020-10-27 | Rename misc nonterminals | Jim Fehrle | |
| 2020-10-12 | Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol | coqbot-app[bot] | |
| Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego | |||
| 2020-10-09 | Add an XML message for "Show Proof Diffs" | Jim Fehrle | |
| Add menu item that uses this | |||
| 2020-10-08 | Dropping the misleading int argument of Pp.h. | Hugo Herbelin | |
| An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended. | |||
| 2020-10-08 | Add a check of empty list of arguments in xmlprotocol where relevant. | Hugo Herbelin | |
| 2020-09-27 | Recognize only ":{{" as a sentence-gobbling quotation. | Guillaume Melquiond | |
| 2020-09-22 | Setting default value for Display Parentheses off in CoqIDE. | Hugo Herbelin | |
| 2020-09-01 | Unify the shelves | Maxime Dénès | |
| Before this patch, the proof engine had three notions of shelves: - A local shelf in `proofview` - A global shelf in `Proof.t` - A future shelf in `evar_map` This has lead to a lot of confusion and limitations or bugs, because some components have only a partial view of the shelf: the pretyper can see only the future shelf, tactics can see only the local and future shelves. In particular, this refactoring is needed for #7825. The solution we choose is to move shelf information to the evar map, as a shelf stack (for nested `unshelve` tacticals). Closes #8770. Closes #6292. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-08-26 | Move given_up goals to evar_map | Maxime Dénès | |
| 2020-08-06 | Repair coqide option "Display parentheses" | Jean-Christophe Léchenet | |
| 2020-06-29 | Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:() | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-06-26 | [declare] Reify Proof.t API into the Proof module. | Emilio Jesus Gallego Arias | |
| This is in preparation for the next commit which will clean-up the current API flow in `Declare`. | |||
| 2020-06-23 | CoqIDE: fix lexing of UTF-8 in quotations like constr:() | James Lottes | |
| 2020-06-22 | CoqIDE: accept to open files with invalid names | Vincent Laporte | |
| 2020-06-02 | Move CoqIDE to its own folder | Maxime Dénès | |
| The will make it possible to put a VsCoq toplevel in `ide/vscoq`. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |