| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-14 | Revert "Fixing bug #3817." | Pierre-Marie Pédrot | |
| This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2. | |||
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-07 | Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE ↵ | Hugo Herbelin | |
| buffer. | |||
| 2014-12-07 | Ensuring that ide_slave and stm receive only .v files from CoqIDE. | Hugo Herbelin | |
| In particular, renouncing to original support for existing non .v files in CoqIDE (hoping it is ok for anyone). Please amend if better to propose. | |||
| 2014-12-01 | Remove dead code | Enrico Tassi | |
| 2014-11-27 | Feedback: API cleaned up, documented and made user extensible | Enrico Tassi | |
| 2014-11-24 | Fixing bug #3817. | Pierre-Marie Pédrot | |
| Coqtop was wrongly assuming that receiving a SIGINT when reading on a channel meant that the channel was closed, resulting in a crash when interrupting an idle coqtop from CoqIDE. To prevent this, we block SIGINTs when reading in ide_slave. | |||
| 2014-11-15 | Reworking the -color flag of coqtop. | Pierre-Marie Pédrot | |
| 2014-11-06 | Fixing compilation (name of module Richprinter) I partially feel | Hugo Herbelin | |
| responsible about. | |||
| 2014-11-04 | ide/Xmlprotocol: Cosmetics. | Yann Régis-Gianas | |
| 2014-11-04 | ide/Ide_slave.annotate: Implement annotate. | Regis-Gianas | |
| 2014-11-04 | ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between ↵ | Regis-Gianas | |
| internal and external datatypes. | |||
| 2014-11-04 | ide/wg_ProofView: Do not refer to the {Proof} internal module, use ↵ | Regis-Gianas | |
| {Interface} instead. | |||
| 2014-11-04 | ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate". | Regis-Gianas | |
| - Extend the protocol with a new command called "annotate". - By the way, relax the dependencies between the "ide" package and the internal packages of Coq by *not* referring to external type definitions inside Interface. Indeed, the purpose of the protocol is to act as a barrier between the source tree of Coq and the source tree of Coqide. We should enforce this property. (Maybe one day coqide will be extracted from the source tree of Coq to live its own life.) | |||
| 2014-10-24 | Install index_urls.txt in a location where coqide might actually find it. | Guillaume Melquiond | |
| 2014-10-24 | Fixing order of hypothesis in goal hypotheses compaction for coqtop. | Hugo Herbelin | |
| 2014-10-23 | fix parsing of ---- +++++ ***** in CoqIDE | Enrico Tassi | |
| 2014-10-22 | Pushing Pierre's factorization of names in goal context printing from | Hugo Herbelin | |
| coqide to coqtop. (Joint work with Pierre) | |||
| 2014-10-22 | CoqIDE: fix parsing of multicharacter bullets | Enrico Tassi | |
| 2014-10-22 | Fix the way lexeme start is computed (Close 3737) | Enrico Tassi | |
| 2014-10-01 | STM: report the (structured) goals as XML | Carst Tankink | |
| The leafs of the XML trees are still pretty-printed strings, but this could be refined later on. | |||
| 2014-10-01 | Factored out IDE goal structure. | Carst Tankink | |
| The more structured goal record type of CoqIDE is also useful for other interfaces (in particular, for PIDE). To support this, the datatype was factored out to the Proof module. In addition, the record gains a type parameter, to allow interfaces to adapt the output to their needs. To accommodate this type, the Proof module also gains the map_structured_proof that takes a Proof.proof and a function on the individual goals (in the context of an evar map) and produces a structured goal based on the goal transformer. | |||
| 2014-09-29 | CoqIDE: new message to print AST | Enrico Tassi | |
| 2014-09-17 | Remove pointless regex for '""' as the empty string already matches it. | Guillaume Melquiond | |
| 2014-09-17 | Fix highlighting of "Hint Unfold" and "Hint Rewrite". | Guillaume Melquiond | |
| 2014-09-17 | Properly highlight the Export keyword. | Guillaume Melquiond | |
| 2014-09-17 | Fix ambiguous regex in syntax highlighting. | Guillaume Melquiond | |
| This fix considerably speeds up syntax highlighting. It also avoids burning 100% CPU when typing long identifiers. Finally, identifiers longer than 20 characters are now properly highlighted, since the stack of the automaton no longer overflows because of them. | |||
| 2014-09-17 | Fix broken syntax highlighting for Coq files using "Proof constr". | Guillaume Melquiond | |
| See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof. | |||
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | |
| instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions. | |||
| 2014-09-09 | IDE: escape popup text (close: 3600) | Enrico Tassi | |
| 2014-09-09 | IDE: disable editable text area underline when -debug | Enrico Tassi | |
| This way a user *can* use coqide with -debug | |||
| 2014-09-09 | toploop plugins taken into account when printing --help (close: 3535) | Enrico Tassi | |
| E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE | |||
| 2014-09-04 | Add a [Variant] declaration which allows to write non-recursive variant types. | Arnaud Spiwack | |
| Just like the [Record] keyword allows only non-recursive records. | |||
| 2014-09-02 | Fixup introduction of coqworkmgr | Pierre Boutillier | |
| 2014-09-02 | coqworkmgr | Enrico Tassi | |
| 2014-09-01 | Coqide prints succesive hyps of the same type on 1 line | Pierre Boutillier | |
| This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention". | |||
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar). | |||
| 2014-08-24 | Fixing bug #3404. | Pierre-Marie Pédrot | |
| 2014-08-24 | Enabling drag & drop on the source view widgets. | Pierre-Marie Pédrot | |
| Sort of fixes bug #2765, but the file loading is broken and puts coqtop in an inconsistent state, so that even the previous half-working patch was actually not functionning at all. This should be fixed eventually. | |||
| 2014-08-12 | Quick fix for avoiding infinitely many respawning and Warning "Coq | Hugo Herbelin | |
| died" when coqtop or coqtopide.cmxs are in inconsistent state. | |||
| 2014-08-05 | CoqIDE: fixing parsing of bullets and brackets even at end of file. | Hugo Herbelin | |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | |
| 2014-08-05 | Coqide: check_connection now also checks correct loading of coqide plugin + | Hugo Herbelin | |
| reports errors also from stderr. | |||
| 2014-08-05 | STM: code restructured to reuse task queue for tactics | Enrico Tassi | |
| 2014-08-05 | Coqide: annoying popups with GTK errors only in debug mode | Enrico Tassi | |
| 2014-07-24 | Make MacStore like coqide more | Pierre Boutillier | |
| including bigger icons | |||
| 2014-07-22 | Ide: Drop argument added by MacOS during .app launch | Pierre Boutillier | |
| 2014-07-22 | the art of forgetting new files during rebase -i | Pierre Boutillier | |
| 2014-07-22 | A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundle | Pierre Boutillier | |
| The created bundle contains only coqide and gtk (no coqtop, no stdlib) | |||
| 2014-07-22 | Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file exists | Pierre Boutillier | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |