index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
ide
/
ideproof.ml
Age
Commit message (
Expand
)
Author
2012-07-16
Added abstration layer to goal display in CoqIDE, and cleaned parts
ppedrot
2012-07-16
Fixing goal display when still focussing but no more goals.
ppedrot
2012-07-10
Adapting the IDE interface with the focussed display.
ppedrot
2012-05-23
Revert copy/pasted function in to minilib thanks to clib.cma
pboutill
2012-05-23
Fixed #2782.
ppedrot
2012-04-18
Renamed end-of-proof message by a less disturbing one.
ppedrot
2012-04-14
Coqide Proofview scroll
pboutill
2012-04-12
Coqide minor enhancements
pboutill
2011-12-15
Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...
ppedrot
2011-11-25
Separated the toplevel interface into a purely declarative module with associ...
ppedrot
2011-11-18
Return of the tactic hints features in CoqIDE.
ppedrot
2011-11-18
Now Coqtop has a richer way to answer a query about its pending goals. Answer...
ppedrot
2011-11-18
Replaced goal api call with a proper structure. This disables menu hints in C...
ppedrot
2011-03-25
Ide: more reorganisation and cleanup
letouzey
2011-03-23
Ide: stronger separation from coqtop
letouzey
2010-09-28
Fix function applications without labels (OCaml warning 6)
glondu
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-05-31
deporting Coq specific code from ide to toplevel.
vgross
2010-05-04
- Fixing bug #2308 about Lemma ... with
vsiles
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2010-04-05
Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflit
aspiwack