coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Revert "New evar_map printer ppevmfull which can typically be installed for"	herbelin	2011-10-17
*	New evar_map printer ppevmfull which can typically be installed for	herbelin	2011-10-17
*	dev/base_include: display a nice message at the end of the load	letouzey	2011-10-15
*	debugging.txt: no more typing of #use "include" if using .ocamlinit	letouzey	2011-10-15
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin	2011-10-01
*	Polishing commits r14492, r14448 and r14407 (tactics propagate	herbelin	2011-09-25
*	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau	2011-08-04
*	Add printer dependency to Hashtbl_alt (used in Term)	puech	2011-07-29
*	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin	2011-07-18
*	Finally, pr_goal seems to work for printing v8.2 style goal in debugger.	herbelin	2011-07-16
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	A few comments and a dev file to summarize issues with unification	herbelin	2011-06-13
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	As many notation for for vectors as for List.	pboutill	2011-05-03
*	dev/base_include: no more mod_self_id	letouzey	2011-04-26
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Fix dev/base_include after change of constant_body	letouzey	2011-04-06
*	Adapt printers.mllib after my last commit	letouzey	2011-03-16
*	Annotations at functor applications:	letouzey	2011-02-11
*	Update changelogs	glondu	2011-02-11
*	Factorize code of rewrite to make way for a new implementation using the	msozeau	2011-02-07
*	Remove obsolete script univdot, update dev doc about universes	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Prepare change of nomenclature rawconstr -> glob_constr	glondu	2010-12-23
*	Print universes in debugging printers	glondu	2010-11-08
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Remove Explain* vernacs	glondu	2010-10-06
*	Install a printer for fconstr (ppconstr was installed twice)	glondu	2010-10-04
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Updated COPYRIGHT file and header. Improved and fixed header updater.	herbelin	2010-07-24
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	Turned off Mac dynlink hack for 10.6.3+ on x86_64	thutchin	2010-07-05
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Names: remove obsolete mod_self_id	letouzey	2010-06-23
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Quick fix for having clenv debug printer working in trunk.	herbelin	2010-06-18
*	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin	2010-06-14
*	Fixed a bug in pretty-printing "induction" and "destruct" due to a	herbelin	2010-06-13
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Added debugging printer for the idmap used at evar definition time for	herbelin	2010-06-12
*	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin	2010-06-09
*	Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)	glondu	2010-06-07
*	Updated performance analysis file	herbelin	2010-06-06