aboutsummaryrefslogtreecommitdiff
path: root/ide/ideproof.ml
AgeCommit message (Expand)Author
2012-07-16Added abstration layer to goal display in CoqIDE, and cleaned partsppedrot
2012-07-16Fixing goal display when still focussing but no more goals.ppedrot
2012-07-10Adapting the IDE interface with the focussed display.ppedrot
2012-05-23Revert copy/pasted function in to minilib thanks to clib.cmapboutill
2012-05-23Fixed #2782.ppedrot
2012-04-18Renamed end-of-proof message by a less disturbing one.ppedrot
2012-04-14Coqide Proofview scrollpboutill
2012-04-12Coqide minor enhancementspboutill
2011-12-15Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...ppedrot
2011-11-25Separated the toplevel interface into a purely declarative module with associ...ppedrot
2011-11-18Return of the tactic hints features in CoqIDE.ppedrot
2011-11-18Now Coqtop has a richer way to answer a query about its pending goals. Answer...ppedrot
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in C...ppedrot
2011-03-25Ide: more reorganisation and cleanupletouzey
2011-03-23Ide: stronger separation from coqtopletouzey
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-31deporting Coq specific code from ide to toplevel.vgross
2010-05-04 - Fixing bug #2308 about Lemma ... withvsiles
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-05Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflitaspiwack