coq - The formal proof system

Age	Commit message (Expand)	Author
2009-08-23	Fix a small oversight in checker commit 12288.	herbelin
2009-08-22	Transfers to checker ("let"s in inductive arities + Coq root read-only).	herbelin
2009-08-20	new csdp cache + improved error message	fbesson
2009-08-20	new csdp cache + improved error message	fbesson
2009-08-19	adds a property on map	bertot
2009-08-19	adds lemmas on interactions between existsb, forallb, and app	bertot
2009-08-15	+ csdp.cache	fbesson
2009-08-14	Mise à jour du document de révision de la stdlib et déplacement de la	herbelin
2009-08-14	+Fix interface.	aspiwack
2009-08-14	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack
2009-08-14	Added profile.cmo in grammar.cma so that any functions in one of the	herbelin
2009-08-14	Tried to make F1 documentation tool working in CoqIDE.	herbelin
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-13	Made unification patch 12268 even more ad hoc (if evars remain in a	herbelin
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-08-11	Ajout des .annot dans le .gitignore.	aspiwack
2009-08-11	Fixed extra space in printing notation { x & P } + minor other things	herbelin
2009-08-11	Infix (r12268 continued)	herbelin
2009-08-11	Add support for "Infix ... := constr" instead of just "Infix ... := ref".	herbelin
2009-08-11	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin
2009-08-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin
2009-08-06	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	Move out JMeq of subst for compatibility (it affects e.g. the	herbelin
2009-08-05	changed deprecated setoid into relation	amahboub
2009-08-04	- Add more precise error localisation when one of the application fails	herbelin
2009-08-04	Fixed subst failing when a truly heterogeneous JMeq hyp is in the	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-08-02	Fixed a typo in "info" for tactic "right".	herbelin
2009-08-01	csdpcert + unix	fbesson
2009-07-31	addition of lia.cache - csdp.cache is now handled by micromega not csdpcert	fbesson
2009-07-30	micromega : Better parsing of formulae - smaller proof terms for Z - redesign...	fbesson
2009-07-30	psatz Z -> psatz Z 1	fbesson
2009-07-30	Git ignore files	herbelin
2009-07-30	For git users, a global .gitignore file	letouzey
2009-07-24	OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith	letouzey
2009-07-24	List: add a iff-based lemma about In and ++	letouzey
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-07-22	Better comparison functions in OrderedTypeEx	letouzey
2009-07-20	Use unfold directly in unfold_equations. Fixes test-suite.	msozeau
2009-07-20	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	Typo in a comment	letouzey
2009-07-15	- Granted wish #2138 (support for local binders in syntax of Record fields).	herbelin
2009-07-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin
2009-07-14	Simplify eauto and fix it for compatibility, allowing full delta during	msozeau
2009-07-09	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau
2009-07-09	Allow coqdoc comments inside definition bodies.	msozeau
2009-07-09	Correction bug 2134.	soubiran