| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-05-05 | Compatibility ocaml 3.12. | Hugo Herbelin | |
| 2015-05-05 | Granting wish #4221. | Pierre-Marie Pédrot | |
| 2015-04-27 | Improve syntax highlighting. | Guillaume Melquiond | |
| - Arithmetic operators and brackets are no longer recognized as bullets, unless they follow a stop or start a line. - Most vernacular commands are no longer highlighted when used inside proof scripts. - Coqdoc comments now take precedence over regular comments. | |||
| 2015-04-26 | Open the file chooser even if there is no current session. (Fix bug #4206) | Guillaume Melquiond | |
| 2015-04-09 | Add extraction to JSON. | Nickolai Zeldovich | |
| This patch allows Coq terms to be extracted into the widely used JSON format. This is useful in at least two cases: - One might want to manipulate Coq values outside of Coq, but without being forced to use one of the three existing extraction languages (OCaml, Haskell, or Scheme), and without having to compile Coq's extracted result. This is especially useful when a Coq evaluation produces some data structure that needs to be moved out of Coq. Having to invoke an OCaml/Haskell/Scheme compiler just to get a data structure out of Coq is somewhat awkward. - One might want to experiment with extracting Coq code into other languages (Go, Javascript, etc), without having to write the whole extraction logic in OCaml and recompile Coq's extraction plugin each time. This makes it easy to quickly prototype extraction in any language, without having to build Coq from source. Extraction to JSON is implemented by adding the JSON "pseudo-language" to the extraction facility. Thus, one can extract the JSON encoding of a single term using: Extraction Language JSON. Extraction qualid. and extract an entire Coq library "ident" into "ident.json" using: Extraction Language JSON. Extraction Library ident. Nota (Pierre Letouzey) : this is an updated version of the original PullRequest, updated to match recent changes in trunk | |||
| 2015-04-03 | Use the directory of the current session for selecting files to open. | Guillaume Melquiond | |
| The old behavior was extremely annoying, especially when using coqide from the command line, since the "open" box would then point to a seemingly random point of the filesystem rather than to the directory of the files currently being edited (since they were passed on the command line rather than by point-and-click). The new behavior matches the one of mainstream editors, e.g. emacs, gedit. | |||
| 2015-04-02 | CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168) | Enrico Tassi | |
| No "read-only" terminator. If no terminator is present the UI complains. If the terminator is different, STM warns but continues. The STM warns that the "check the document" button will not honor the terminator change, and what to do to avoid that. Technically, one cannot turn (a posteriori) an axiom into a theorem and vice versa. Could be done, but not with a small patch. | |||
| 2015-03-11 | CoqIDE: load first _CoqProject file found and notify the user | Enrico Tassi | |
| 2015-03-11 | CoqIDE: fix tag colors to support superposing unsafe and partial | Enrico Tassi | |
| Admitted (like Qed) can be "partially executed", but is also unsafe. | |||
| 2015-03-11 | CoqIDE: restore module/proof name in info bar | Enrico Tassi | |
| 2015-03-11 | CoqIDE: do not lose tag on Qed ending focused proof | Enrico Tassi | |
| 2015-03-06 | Simplify grammar for syntax highlighting by removing extraneous parentheses. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Print/Reset Extraction. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Extraction Inline and add Separate Extraction. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Extraction Language. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Typeclasses Opaque. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Module (Type). | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Extract Inductive. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for Declare Module. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Import and Export. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for Declare ML Module. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Require. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Scheme. | Guillaume Melquiond | |
| 2015-03-06 | Do not highlight "using" as a constr keyword. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for About. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Save. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context. | Guillaume Melquiond | |
| 2015-03-06 | Add syntax highlighting for Coercion. | Guillaume Melquiond | |
| 2015-03-06 | Fix syntax highlighting of "Require multiple libraries". | Guillaume Melquiond | |
| 2015-02-25 | CoqIDE: correclty unfocus (remove all tags) when jumping out of a proof | Enrico Tassi | |
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond | |
| 2015-02-20 | Fixing bug #4073. | Pierre-Marie Pédrot | |
| 2015-02-17 | Remove Whelp commands. | Maxime Dénès | |
| Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive. | |||
| 2015-02-17 | Fixing bug #4023 again. | Pierre-Marie Pédrot | |
| 2015-02-17 | Tentative fix for bug #2855. | Pierre-Marie Pédrot | |
| 2015-02-17 | CoqIDE: read-only Qed sentence reflected in colors (Close: 4051) | Enrico Tassi | |
| 2015-02-15 | Fixing bug #4037. | Pierre-Marie Pédrot | |
| 2015-02-15 | Changing default for CoqIDE project to append arguments. | Pierre-Marie Pédrot | |
| Implement wish #3582. | |||
| 2015-02-15 | CoqIDE now remembers the path of the last opened project. | Pierre-Marie Pédrot | |
| Fixes bug #2762. | |||
| 2015-02-15 | Selecting whole words on double-click in CoqIDE. | Pierre-Marie Pédrot | |
| Fixes bug #4026. | |||
| 2015-02-14 | CoqIDE: restore old default colors | Enrico Tassi | |
| 2015-02-14 | Attempt to be more colorblind friendly in CoqIDE (Close #4024) | Enrico Tassi | |
| 2015-02-13 | Fixup version & copyright for MacOS bundle | Pierre Boutillier | |
| 2015-02-13 | Hardcode how coqide have to look for coqtop in MacOS bundle | Pierre Boutillier | |
| Sorry, that is ugly. Please revert if you see a better way to do it. | |||
| 2015-02-13 | Selection of the current word in CoqIDE looks at all buffers. | Pierre-Marie Pédrot | |
| 2015-02-13 | Trying to fix bug #3930. | Pierre-Marie Pédrot | |
| Instead of setting the last modified part of the text to be the insert point, we register all modifications to the buffer between to user actions and take the last modified point to be the least offset of all those modifications. | |||
| 2015-02-12 | Tentative fix for CoqIDE randomly dropping deletions. | Pierre-Marie Pédrot | |
| We make the deletion callback not to regenerate a task id, as the insertion callback does. I can't find a particular reason for this dissymetry, and it was indeed causing trouble. | |||
| 2015-02-12 | Fixing bug #3261. | Pierre-Marie Pédrot | |
| 2015-02-12 | Focussing on message view in CoqIDE when a message is pushed. | Pierre-Marie Pédrot | |
| Also fixes bug #4030. | |||
| 2015-02-12 | Fixing bug #4023. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |