aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
Commit message (Expand)AuthorAge
...
* Separated the toplevel interface into a purely declarative module with associ...Gravatar ppedrot2011-11-25
* Return of the tactic hints features in CoqIDE.Gravatar ppedrot2011-11-18
* Also sprach CoqIDE (in XML)Gravatar ppedrot2011-11-06
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
* Ide_intf: slight reorganisation of the IDE apiGravatar letouzey2011-09-05
* safe_prerr_endline in MinilibGravatar pboutill2011-09-01
* Coqide: try to properly send interrupts to coqtop on Win32Gravatar letouzey2011-04-28
* Coqide: let's try to be synchronuous when killing coqtopGravatar letouzey2011-04-21
* Coqlib: avoid deadlock under win32 with force_reset_initialGravatar letouzey2011-04-21
* Coqide: back to using Unix.stderr in create_processGravatar letouzey2011-04-21
* Coqide: better handling of stdout/stderr in win32Gravatar letouzey2011-04-21
* Coqide: quote coqtop filename if necessaryGravatar letouzey2011-04-21
* Coqide: a special kill function for win32Gravatar letouzey2011-04-21
* Coqide: try to avoid displaying error messages on coqide's consoleGravatar letouzey2011-04-21
* Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ...Gravatar letouzey2011-04-21
* Coqide: avoid confusion of process when restarting coqtop + cosmeticGravatar letouzey2011-03-30
* Ide_slave: better handling of Ctrl-CGravatar letouzey2011-03-30
* Ide: misc (nicer message than End_of_file, a useless try removedGravatar letouzey2011-03-28
* Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsGravatar letouzey2011-03-28
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
* Ide_intf : change type of location in ideGravatar letouzey2011-03-25
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
* Ide: experimentally allow coqide to interrupt or kill coqtopGravatar letouzey2011-03-23
* Call coqtop with -nois when probing for filesGravatar pboutill2011-01-07
* Reverted r13715 "Add improved indenters that rely on the current proof state ...Gravatar gmelquio2011-01-06
* Remove Safe_marshalGravatar glondu2011-01-06
* Add improved indenters that rely on the current proof state to choose the ind...Gravatar gmelquio2010-12-14
* Made new comm. model between coq and coqide support '-R foo ""'-style option.Gravatar herbelin2010-12-04
* Improved error messages in CoqIDE:Gravatar herbelin2010-11-07
* CoqIDE argv parsing delegated to coqtopGravatar vgross2010-09-14
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* coqide: s/Sys.argv.(0)/Sys.executable_name/ for coqtop (cf #2341)Gravatar glondu2010-07-12
* Robustness fix : clean restart of coqtop on pipe error + force matchingGravatar vgross2010-07-05
* Stronger checks on coqtop termination, warning when zombies.Gravatar vgross2010-07-05
* Fixing tabs closing problems by removing activation infrastructure.Gravatar vgross2010-07-02
* fixing error message display.Gravatar vgross2010-06-07
* added -args option to coqide to pass options to coqtopsGravatar vgross2010-06-01
* CoqIDE goes multiprocessGravatar vgross2010-05-31
* More indirection.Gravatar vgross2010-05-31
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
* Modifying startup sequenceGravatar vgross2010-05-31
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Fix bug #2315 : printing of defined evars in Coqide.Gravatar aspiwack2010-05-07
* Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofGravatar pboutill2010-05-05
* Fail: a way to check that a command is refused without blocking a scriptGravatar letouzey2010-04-30
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* 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