coq - The formal proof system

Age	Commit message (Collapse)	Author
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
	instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
2014-09-09	toploop plugins taken into account when printing --help (close: 3535)	Enrico Tassi
	E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
2014-09-02	Fixup introduction of coqworkmgr	Pierre Boutillier

2014-09-02	coqworkmgr	Enrico Tassi

2014-09-01	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier
	This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention".
2014-06-25	all coqide specific files moved into ide/	Enrico Tassi
	lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/