coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	avoid relying on weak invariant in cbv.ml	bgregoir	2011-11-25
*	Added a function to inspect current option state.	ppedrot	2011-11-24
*	Fixed the XML parser CDATA handling (and changed the EOL convention of these ...	ppedrot	2011-11-24
*	Fixed some missing options from previous commit.	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-24
*	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack	2011-11-23
*	Adds a pair of function in Evar_util to gather dependent evars in an	aspiwack	2011-11-23
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	Configurable simpl tactic	gareuselesinge	2011-11-21
*	coqide default pref files are by default in /etc/xdg/coq/	pboutill	2011-11-21
*	/home/pirbo/.coqrc* are read again	pboutill	2011-11-21
*	-user option removal	pboutill	2011-11-21
*	Updated CHANGES file wrt to pattern-matching compilation.	herbelin	2011-11-21
*	Extend the computation of dependencies in pattern-matching compilation	herbelin	2011-11-21
*	Add matching on non-inductive types in building an inversion problem	herbelin	2011-11-21
*	Old naming bug in pattern-matching compilation: names in the	herbelin	2011-11-21
*	Inlining let-in (i.e. trace of aliases) in extract_predicate for what	herbelin	2011-11-21
*	VectorDef.v takes benefit of dependencies being taken into account	herbelin	2011-11-21
*	In pattern-matching compilation, now taking into account the dependencies	herbelin	2011-11-21
*	Optimizing the compilation of unused aliases in pattern-matching.	herbelin	2011-11-21
*	Simplifying history management in pattern-matching compilation.	herbelin	2011-11-21
*	Fixing postprocessing bugs in pattern-matching compilation.	herbelin	2011-11-21
*	Removing stuff about alias dependencies now become useless.	herbelin	2011-11-21
*	Changed the way to detect if an "as" patterns is expanded or not. The	herbelin	2011-11-21
*	Updating Cases.v test.	herbelin	2011-11-21
*	Dead code + refreshing some comments in cases.ml.	herbelin	2011-11-21
*	Typo	herbelin	2011-11-21
*	CHANGES update	pboutill	2011-11-20
*	coqrc in the right XDG_CONFIG_HOME/coq folder	pboutill	2011-11-20
*	coqide-gtk2rc not dotted	pboutill	2011-11-20
*	CoqIdE configuration file won't pollute your home anymore	pboutill	2011-11-20
*	Teach coq_makefile how to install into XDG_DATA_HOME.	pboutill	2011-11-20
*	Add support for XDG_DATA_HOME and XDG_DATA_DIRS.	pboutill	2011-11-20
*	coq_makefile: Don't install with +x.	pboutill	2011-11-20
*	coq_makefile: Add Makefile variables specifying install	pboutill	2011-11-20
*	Adding the type infrastructure to handle properly API management of options	ppedrot	2011-11-18
*	Fix parsing of :>> and backtrack correctly on the cache of hints for local co...	msozeau	2011-11-18
*	Return of the tactic hints features in CoqIDE.	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
*	Added a printing function to handle single evars	ppedrot	2011-11-18
*	Replaced goal api call with a proper structure. This disables menu hints in C...	ppedrot	2011-11-18
*	Coqide -debug only printed Coqtop information.	pboutill	2011-11-18
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18