index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
Age
Commit message (
Expand
)
Author
2011-12-21
sequel of previous commit
letouzey
2011-12-21
Pure interfaces shouldn't be mentionned in .mllib
letouzey
2011-12-19
Arguments: check rename even if no implicit is specified
gareuselesinge
2011-12-17
Command Arguments: standardizing format of error messages and American spelling.
herbelin
2011-12-17
Deactivated automatic inference of _case schemes, as it was in 8.3
herbelin
2011-12-17
A pass on warning printings. Made systematic the use of msg_warning so
herbelin
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-12-06
Minor fixes to Arguments
gareuselesinge
2011-11-30
More type safety in query GADT (again).
ppedrot
2011-11-30
Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enf...
ppedrot
2011-11-29
Fixed a warning about unused variable introduced in r14731
ppedrot
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-24
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-24
Moving XML handling to lib directory
ppedrot
2011-11-24
Correct direction for definitional typeclasses
msozeau
2011-11-21
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
New Arguments vernacular
gareuselesinge
2011-11-21
/home/pirbo/.coqrc* are read again
pboutill
2011-11-21
-user option removal
pboutill
2011-11-20
coqrc in the right XDG_CONFIG_HOME/coq folder
pboutill
2011-11-20
Add support for XDG_DATA_HOME and XDG_DATA_DIRS.
pboutill
2011-11-18
Adding the type infrastructure to handle properly API management of options
ppedrot
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-18
Restore backward compatibility. ":>" declares subinstances in Class declarati...
msozeau
2011-11-17
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-14
Bug 2637: patches to make slightly easier to write programs that use coq code...
pboutill
2011-11-14
Bug 2636 - Move string_of_ppcmds to Pp
pboutill
2011-11-07
Fixed xml-light handling of whitespace not compliant with XML standard: it st...
ppedrot
2011-11-06
Also sprach CoqIDE (in XML)
ppedrot
2011-11-06
Fixed nasty bug when empty PCData, confusion no string vs. empty string
ppedrot
2011-11-06
More XML marshalling functions
ppedrot
2011-11-06
Partialliy added XML marshalling to ide_intf
ppedrot
2011-11-06
Added XML manipulation tools to compilation chain
ppedrot
2011-11-06
Added XML manipulation basics (modified from xml-light)
ppedrot
2011-11-05
Added missing printing debug functions in IDE interface
ppedrot
2011-11-02
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-10-29
Added checksums to glob files and warned about possibly missing
herbelin
2011-10-28
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-25
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-11
Various simplifications about constant_of_delta and mind_of_delta
letouzey
2011-10-08
Scheme names: Use unprobable names + ensure names do not hide existing names
herbelin
2011-10-07
Fix bug #2557 and an issue with Propers for complement
msozeau
2011-10-05
Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).
herbelin
[next]