aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Expand)AuthorAge
* "make source-doc" builds documentation of mli in html and pdf atGravatar pboutill2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Dont recompute the contents of the proof window when entering theGravatar vgross2010-04-28
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
* Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflitGravatar aspiwack2010-04-05
* Changing types to reflect futur separation between toplevel and ide.Gravatar vgross2010-03-23
* Goal generation deported into ide/coq.ml, single function to obtainGravatar vgross2010-03-23
* New functions for goals fetching.Gravatar vgross2010-03-23
* Fix bug in backtracking.Gravatar vgross2010-03-23
* debuggingGravatar vgross2010-03-23
* New backtracking code + fix bug #2082.Gravatar vgross2010-02-26
* Introducing a dual stack setupGravatar vgross2010-02-26
* New API for backtracking.Gravatar vgross2010-02-26
* Redispatch of printing tweaking hooks.Gravatar vgross2010-02-26
* Various fixes in interp, session switching and backtrackingGravatar vgross2010-02-25
* Changes in lexing and tagging.Gravatar vgross2010-02-25
* Fixing compilation issuesGravatar vgross2010-02-19
* Fixing modules names.Gravatar vgross2010-02-18
* Adding uim filesGravatar vgross2010-02-18
* Polishing the setup of CoqIDE Input MethodGravatar vgross2010-02-18
* Change the customization of modifiers (bug #2210)Gravatar vgross2010-02-15
* Simplify backtrackingGravatar vgross2010-02-12
* Delineating a API for Coq inside toplevel/vernac.mlGravatar vgross2010-02-12
* Refactoring of the printing optionsGravatar vgross2010-02-12
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Fix uncaught exceptionGravatar vgross2010-01-14
* Revert "Isolation of proof-displaying code"Gravatar vgross2010-01-11
* Isolation of proof-displaying codeGravatar vgross2010-01-11
* Patches and instructions to enable Input Method support in CoqIDE.Gravatar vgross2009-12-21
* Deport the backtracking code out of the ideGravatar vgross2009-12-11
* Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...Gravatar letouzey2009-12-08
* Fix bug #2197 (option show_toolbar not taken into account at startup)Gravatar vgross2009-12-07
* Remove the "detach script windows" feature.Gravatar vgross2009-12-07
* Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1Gravatar vgross2009-12-03
* Ergonomy and robustness fixGravatar vgross2009-11-23
* Refactoring of coqide backtrack code, with the intent to put everythingGravatar vgross2009-11-19
* Remove dubious call to Obj.magic (and dead code, by the way)Gravatar glondu2009-11-13
* Remove useless call to Obj.magicGravatar glondu2009-11-13
* scripting area now grabs focus at startup.Gravatar vgross2009-11-13
* new handling for lexical structures.Gravatar vgross2009-11-13
* lexing refactoringGravatar vgross2009-11-13
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Removed 'Toplevel' language from extraction documentation, since it is not cu...Gravatar gmelquio2009-11-04
* Added Coqide highlighting for extraction vernacular.Gravatar gmelquio2009-10-30
* Removed 'dest' from keyword highlighting.Gravatar gmelquio2009-10-30
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Added syntactic coloration for 'Function'.Gravatar gmelquio2009-10-20
* note for later : when the tag table is shared, never, ever create twoGravatar vgross2009-10-16