| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-07-10 | CoqIDE: on win32 the old interrputer code (SIGINT) is still needed | Enrico Tassi | |
| 2014-06-30 | Little coqide bug, when coqtop outputs empty lines, as e.g. when calling ↵ | Hugo Herbelin | |
| coqide --help. | |||
| 2014-06-30 | Coq_makefile takes advantages of -I -Q -R cleanup | Pierre Boutillier | |
| 2014-06-30 | Coq_makefile: -extra[-phony] correction + doc | Pierre Boutillier | |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi | |
| lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/ | |||
| 2014-06-19 | Support dropping files over the coqide window. (Partial fix for bug #2765) | Guillaume Melquiond | |
| The fix is only partial, because dropping files only works over the menu bar, the icon bar, the status bar, and so on. Editable boxes, such as the script widget, catch dnd events, hence preventing this code from working for these drop targets. Some (labl)gtk expert should be able to sort it out. | |||
| 2014-05-01 | Fixing ml-doc. | Pierre-Marie Pédrot | |
| 2014-04-28 | Fix broken commit 2bcb2cb. | Guillaume Melquiond | |
| 2014-04-28 | Fix incorrect syntax highlighting after the Goal command. | Guillaume Melquiond | |
| 2014-04-10 | CoqIDE: options for syntax highlighting | Enrico Tassi | |
| 2014-04-10 | CoqIDE: removing a timer may raise an exception | Enrico Tassi | |
| 2014-04-09 | nanoPG: when the cursor moves, scroll to make it appear on screen | Enrico Tassi | |
| 2014-04-09 | nanoPG: takeover keypress only when text view has focus | Enrico Tassi | |
| 2014-04-07 | Allowing proof view to be detached in CoqIDE. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |