index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
/
ide_slave.ml
Age
Commit message (
Expand
)
Author
2012-06-29
Now CoqIDE separates answer and messages. This should hopefully
ppedrot
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-04
Replacing some str with strbrk
ppedrot
2012-06-04
Added a color output to Coqtop.
ppedrot
2012-06-04
Separated notice vs info messages, and cleaned up the interface a bit.
ppedrot
2012-05-29
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-13
Added a SearchAbout-like primitive in coqtop interface.
ppedrot
2012-05-13
Added an interface primitive to ask coqtop for its internal versions.
ppedrot
2012-05-11
Slightly modified the coqtop interface by adding an identifier in
ppedrot
2012-05-02
Added an interface call to exit Coqtop nicely.
ppedrot
2012-04-12
lib directory is cut in 2 cma.
pboutill
2012-03-23
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
Remove undocumented command "Delete foo"
letouzey
2012-03-23
Remove old proof-managment commands Suspend/Resume
letouzey
2012-03-20
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-02
Noise for nothing
pboutill
2012-02-29
Bug 2703: send stdout dump to coqide when an error occurs.
pboutill
2012-02-02
More information returned by coqtop about its internal state. Hopefully we'll...
ppedrot
2011-12-16
Moving bullets (-, +, *) into stand-alone commands instead of being
courtieu
2011-12-15
Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...
ppedrot
2011-12-12
Proof using ...
gareuselesinge
2011-11-25
Added an API call to retrieve and change the option state
ppedrot
2011-11-25
Separated the toplevel interface into a purely declarative module with associ...
ppedrot
2011-11-21
New Arguments vernacular
gareuselesinge
2011-11-18
Added hint support in the API. You can now query a goal to see the tactics th...
ppedrot
2011-11-18
Toplevel loop is a bit more robust: it catches bad API queries.
ppedrot
2011-11-18
Making status info better in CoqIDE: path and name of current lemma
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-11-14
Bug 2636 - Move string_of_ppcmds to Pp
pboutill
2011-11-06
Also sprach CoqIDE (in XML)
ppedrot
2011-09-05
Coqide: new backtracking code, based on the Backtrack command
letouzey
2011-09-05
Ide_intf: slight reorganisation of the IDE api
letouzey
2011-08-18
Misc improvements concerning "Show Match" and its coqide equivalent
letouzey
2011-07-28
Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)
letouzey
2011-07-16
This option disables the use of the '{| field := ... |}' notation
herbelin
2011-05-18
Coqide: allow the use of Abort (grant wish #2357)
letouzey
2011-05-13
A new mechanism to handle errors.
aspiwack
2011-04-21
Coqide: better handling of stdout/stderr in win32
letouzey
2011-04-06
Add 'Existing Instances' declaration to declare multiple instances at once.
letouzey
2011-03-30
Ide_intf: documentation of calls + debug printing of calls/answers
letouzey
2011-03-30
Ide_intf: remove useless int answer to the "interp" and "rewind" calls
letouzey
2011-03-30
Ide_slave: better handling of Ctrl-C
letouzey
2011-03-28
Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_break
letouzey
2011-03-28
Ide_slave: improved handling of exceptions (in particular ^C)
letouzey
2011-03-28
Ide_slave: a more robust current_status () function
letouzey
2011-03-25
Ide_intf : change type of location in ide
letouzey
2011-03-23
Ide: stronger separation from coqtop
letouzey
[prev]