coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-07-08	Fixed bug #2116 ("simpl" created ill-typed term while accepting	herbelin
2009-07-08	Don't use recent ocaml tolerance for pattern "ProjectVar _" when	herbelin
2009-07-08	Simplify addition of hints to a hint_db. Rebuild the dnet associated	msozeau
2009-07-08	Use user-given implicits from the arity in inductive definitions.	msozeau
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-08	Add heuristic based on non-linearity of evars to determine whether an	herbelin
2009-07-08	Fixed anomaly when trying to load non existing file starting with "./" or "../".	herbelin
2009-07-08	Fixing bug 2129 (evar introduced to remember an ambiguous projection	herbelin
2009-07-08	Completing support for F5=About by adding About to the state-preserving comma...	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-07-06	change in the order of unification constraints solving (for canonical structu...	amahboub
2009-07-04	repport of commit r12221	jforest
2009-07-01	Support for binding Coq root read-only in -R option	herbelin
2009-06-30	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau
2009-06-29	Miscellaneous practical commits:	herbelin
2009-06-29	Fix bug introduced by last revision, subtac_cases was returning the	msozeau
2009-06-28	Raise an error and not an anomaly if a rewrite is attempted on a	msozeau
2009-06-28	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-26	propagation sur le trunk du commit 12101	soubiran