aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
Commit message (Expand)AuthorAge
...
* 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
* 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
* 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
* Revert "Isolation of proof-displaying code"Gravatar vgross2010-01-11
* Isolation of proof-displaying codeGravatar vgross2010-01-11
* 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 #2191 : Serious "undo" performance degradation since 8.2pl1Gravatar vgross2009-12-03
* Refactoring of coqide backtrack code, with the intent to put everythingGravatar vgross2009-11-19
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* 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
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* kills the old backtracking framework and replaces it withGravatar vgross2009-09-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14