coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-06-26	Add doc for [Print Opaque Dependencies] and a better explanation for the	msozeau
2009-06-22	Correct treatment of dependent products in signatures: create the evars	msozeau
2009-06-22	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau
2009-06-22	documented a bug of pattern unification with metas	barras
2009-06-22	made several occurrences of (eapply ...; eauto) not rely on the lack of patte...	barras
2009-06-22	Report de la révision #12200 (bug #2125)	notin
2009-06-22	remove some unused functions (which are part of a soon-to-be obsolete	vgross
2009-06-22	clearing unused functions	vgross
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-06-18	Fix "unsatisfiable constraints" error messages to include all the	msozeau
2009-06-18	Try typeclass resolution in coercion if no solution can be found to a	msozeau
2009-06-17	Fallback on not using [fix_proto] if the right imports aren't there, the	msozeau
2009-06-16	Reimplementation of leibniz rewrite to control the instantiation of the	msozeau
2009-06-15	Allow anonymous instances again, with syntax [Instance: T] where T	msozeau
2009-06-13	Correct typo: -noglob takes no argument.	msozeau
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-06-11	Simplifying the call to print_no_goals and not calling it when no goal	herbelin
2009-06-11	When typing a non-dependent arrow, do not put the (anonymous) variable	msozeau
2009-06-10	Accept more Unicode symbols	glondu
2009-06-10	Use the projections for reflexivity, symmetry and transitivity proofs to	msozeau
2009-06-09	Correct handling of the initial existentials from the goal and the ones	msozeau
2009-06-08	Do a fixpoint on the result of typeclass search to force the	msozeau
2009-06-08	Change in UI behaviour : proof folding is now done by double clicking. Delay is	vgross
2009-06-07	File forgotten in commit 12171.	herbelin