aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Expand)AuthorAge
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
* Fixing bug #3817.Gravatar Pierre-Marie Pédrot2014-11-24
* Reworking the -color flag of coqtop.Gravatar Pierre-Marie Pédrot2014-11-15
* Fixing compilation (name of module Richprinter) I partially feelGravatar Hugo Herbelin2014-11-06
* ide/Xmlprotocol: Cosmetics.Gravatar Yann Régis-Gianas2014-11-04
* ide/Ide_slave.annotate: Implement annotate.Gravatar Regis-Gianas2014-11-04
* ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between i...Gravatar Regis-Gianas2014-11-04
* ide/wg_ProofView: Do not refer to the {Proof} internal module, use {Interface...Gravatar Regis-Gianas2014-11-04
* ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate".Gravatar Regis-Gianas2014-11-04
* Install index_urls.txt in a location where coqide might actually find it.Gravatar Guillaume Melquiond2014-10-24
* Fixing order of hypothesis in goal hypotheses compaction for coqtop.Gravatar Hugo Herbelin2014-10-24
* fix parsing of ---- +++++ ***** in CoqIDEGravatar Enrico Tassi2014-10-23
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* CoqIDE: fix parsing of multicharacter bulletsGravatar Enrico Tassi2014-10-22
* Fix the way lexeme start is computed (Close 3737)Gravatar Enrico Tassi2014-10-22
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
* Factored out IDE goal structure.Gravatar Carst Tankink2014-10-01
* CoqIDE: new message to print ASTGravatar Enrico Tassi2014-09-29
* Remove pointless regex for '""' as the empty string already matches it.Gravatar Guillaume Melquiond2014-09-17
* Fix highlighting of "Hint Unfold" and "Hint Rewrite".Gravatar Guillaume Melquiond2014-09-17
* Properly highlight the Export keyword.Gravatar Guillaume Melquiond2014-09-17
* Fix ambiguous regex in syntax highlighting.Gravatar Guillaume Melquiond2014-09-17
* Fix broken syntax highlighting for Coq files using "Proof constr".Gravatar Guillaume Melquiond2014-09-17
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* IDE: escape popup text (close: 3600)Gravatar Enrico Tassi2014-09-09
* IDE: disable editable text area underline when -debugGravatar Enrico Tassi2014-09-09
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
* Fixup introduction of coqworkmgrGravatar Pierre Boutillier2014-09-02
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Fixing bug #3404.Gravatar Pierre-Marie Pédrot2014-08-24
* Enabling drag & drop on the source view widgets.Gravatar Pierre-Marie Pédrot2014-08-24
* Quick fix for avoiding infinitely many respawning and Warning "CoqGravatar Hugo Herbelin2014-08-12
* CoqIDE: fixing parsing of bullets and brackets even at end of file.Gravatar Hugo Herbelin2014-08-05
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Coqide: check_connection now also checks correct loading of coqide plugin +Gravatar Hugo Herbelin2014-08-05
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* Coqide: annoying popups with GTK errors only in debug modeGravatar Enrico Tassi2014-08-05
* Make MacStore like coqide moreGravatar Pierre Boutillier2014-07-24
* Ide: Drop argument added by MacOS during .app launchGravatar Pierre Boutillier2014-07-22
* the art of forgetting new files during rebase -iGravatar Pierre Boutillier2014-07-22
* A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundleGravatar Pierre Boutillier2014-07-22
* Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsGravatar Pierre Boutillier2014-07-22
* CoqIDE: on win32 the old interrputer code (SIGINT) is still neededGravatar Enrico Tassi2014-07-10
* Little coqide bug, when coqtop outputs empty lines, as e.g. when calling coqi...Gravatar Hugo Herbelin2014-06-30
* Coq_makefile takes advantages of -I -Q -R cleanupGravatar Pierre Boutillier2014-06-30
* Coq_makefile: -extra[-phony] correction + docGravatar Pierre Boutillier2014-06-30
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 08:46:41 +0000