aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ide.mllib
Commit message (Expand)AuthorAge
* wg_Detachable: move out of wg_CommandGravatar gareuselesinge2013-10-22
* CoqIDE: cStack -> DocumentGravatar gareuselesinge2013-10-07
* CoqIDE: wg_Tooltip removed, new tooltip handlingGravatar gareuselesinge2013-09-30
* Add a (very minimal) Proof General mode to CoqIDEGravatar gareuselesinge2013-08-08
* Coqide: Globalization feedback (proof of concept)Gravatar gareuselesinge2013-04-25
* New autocompletion mechanism in CoqIDE. Now provides many answersGravatar ppedrot2013-02-19
* Coqide: some more refactoring to lighten coqide.mlGravatar letouzey2012-12-10
* Nice output of SearchAbout command in CoqIDEGravatar ppedrot2012-09-06
* Added abstration layer to goal display in CoqIDE, and cleaned partsGravatar ppedrot2012-07-16
* Made the message view of CoqIDE abstract.Gravatar ppedrot2012-06-24
* Added semantic completion in CoqIDE. (Should also add an option for that...)Gravatar ppedrot2012-05-13
* Rewritten the autocompletion mechanism of CoqIDE, and stuffed itGravatar ppedrot2012-05-08
* Renamed Undo to conform to CoqIDE widget naming convention. In addition,Gravatar ppedrot2012-05-05
* Now CoqIDE has a nice find & replace mechanism. BTW, removing a blob of dead ...Gravatar ppedrot2012-04-23
* Cleaning up widget code and using a naming convention for such files.Gravatar ppedrot2012-04-20
* Add option -f to coqideGravatar pboutill2011-09-01
* Creation of ide/project_file.ml4Gravatar pboutill2011-09-01
* Menubar and toolbar in coqide using GtkUI & Gactions.Gravatar pboutill2011-06-10
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
* Reverted r13715 "Add improved indenters that rely on the current proof state ...Gravatar gmelquio2011-01-06
* Add improved indenters that rely on the current proof state to choose the ind...Gravatar gmelquio2010-12-14
* Remove ide/coq_tactics.ml*Gravatar glondu2010-10-06
* Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflitGravatar aspiwack2010-04-05
* Goal generation deported into ide/coq.ml, single function to obtainGravatar vgross2010-03-23
* Fixing modules names.Gravatar vgross2010-02-18
* Revert "Isolation of proof-displaying code"Gravatar vgross2010-01-11
* Isolation of proof-displaying codeGravatar vgross2010-01-11
* new handling for lexical structures.Gravatar vgross2009-11-13
* tags refactoringGravatar vgross2009-09-14
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20