coq - The formal proof system

Age	Commit message (Expand)	Author
2009-06-22	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-06-17	Fallback on not using [fix_proto] if the right imports aren't there, the	msozeau
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-06-06	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin
2009-05-27	Fix implicit args code so that declarations are added for all	msozeau
2009-05-26	Fix de Bruijn lifting bug appearing when we match on multiple terms with	msozeau
2009-05-16	Support for definition hooks in subtac.	msozeau
2009-05-11	micromega: proof compression bugfix	fbesson
2009-04-28	More efficient handling of evars in Program Fixpoint commands.	msozeau
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-24	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-16	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-08	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-07	Fixes in Program:	msozeau
2009-04-07	Move setoid_rewrite to its own module and do some clean up in	msozeau
2009-04-03	Ocamlbuild: improvements suggested by N. Pouillard	letouzey
2009-03-30	Add a more general quote construction	glondu
2009-03-30	Fix some typos and spaces	glondu
2009-03-29	Csdpcert: adaptation after last commit	letouzey
2009-03-29	Micromega: improvement of the code obtained by extraction	letouzey
2009-03-28	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-27	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey
2009-03-27	GroebnerZ: no more admitted lemmas	letouzey
2009-03-26	Fixes in Program well-founded definitions:	msozeau
2009-03-26	ocamlbuild: coqide, coqchk, a bit of .vo	letouzey
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey