coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	Infix (r12268 continued)	herbelin	2009-08-11
*	Cleaning of Nametab continued + fixed a compilation bug in previous commit.	herbelin	2009-08-06
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Added "etransitivity".	herbelin	2009-08-03
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	addition of lia.cache - csdp.cache is now handled by micromega not csdpcert	fbesson	2009-07-31
*	micromega : Better parsing of formulae - smaller proof terms for Z - redesign...	fbesson	2009-07-30
*	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey	2009-07-24
*	Use camlp4 to accept some specific non-exhaustive patterns in groebner	letouzey	2009-07-20
*	Move some examples for groebner into a test-suite file	letouzey	2009-07-20
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	repport of commit r12221	jforest	2009-07-04
*	Miscellaneous practical commits:	herbelin	2009-06-29
*	Fix bug introduced by last revision, subtac_cases was returning the	msozeau	2009-06-29
*	Abstract the tycon by the matched terms when turning them into variables	msozeau	2009-06-28
*	Improve return predicate inference by making the return type dependent	msozeau	2009-06-28
*	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau	2009-06-22
*	Use more consistent resolution parameters in Program and regular typing	msozeau	2009-06-18
*	Fallback on not using [fix_proto] if the right imports aren't there, the	msozeau	2009-06-17
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin	2009-06-06
*	Fix implicit args code so that declarations are added for all	msozeau	2009-05-27
*	Fix de Bruijn lifting bug appearing when we match on multiple terms with	msozeau	2009-05-26
*	Support for definition hooks in subtac.	msozeau	2009-05-16
*	micromega: proof compression bugfix	fbesson	2009-05-11
*	More efficient handling of evars in Program Fixpoint commands.	msozeau	2009-04-28
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin	2009-04-24
*	- New cleaning phase for the entry points of pretyping.ml	herbelin	2009-04-24
*	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau	2009-04-16
*	nouvelle version de la tactique groebner proposee par Loic:	barras	2009-04-16
*	Experimental support for automatic destruction of recursive calls and	msozeau	2009-04-08
*	Fix bug #2083 for good: verify that the measure and relation are	msozeau	2009-04-08
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	Fixes in Program:	msozeau	2009-04-07
*	Move setoid_rewrite to its own module and do some clean up in	msozeau	2009-04-07
*	Ocamlbuild: improvements suggested by N. Pouillard	letouzey	2009-04-03
*	Add a more general quote construction	glondu	2009-03-30
*	Fix some typos and spaces	glondu	2009-03-30
*	Csdpcert: adaptation after last commit	letouzey	2009-03-29
*	Micromega: improvement of the code obtained by extraction	letouzey	2009-03-29
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Fix static compilation of numeral syntax (typo in _mod files, sorry ...)	letouzey	2009-03-28
*	ZMicromega: useless dependency toward ZArith.Int	letouzey	2009-03-28
*	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey	2009-03-27
*	GroebnerZ: no more admitted lemmas	letouzey	2009-03-27
*	Fixes in Program well-founded definitions:	msozeau	2009-03-26
*	ocamlbuild: coqide, coqchk, a bit of .vo	letouzey	2009-03-26
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20