coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-07	Fix lifting of constraints in generalized rewriting tactic.	msozeau
2010-03-06	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau
2010-03-05	Improvements in generalized rewriting:	msozeau
2010-03-05	Fix [autounfold] to accept general [in] clauses.	msozeau
2010-03-05	Add a generic tactic option builder. Use it in firstorder to set the	msozeau
2010-02-10	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau
2010-01-30	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau
2010-01-26	Support for generalized rewriting under dependent binders, using the	msozeau
2010-01-26	Quick fix for references to section variables unbound in the current	msozeau
2010-01-12	New version of 12650 that was broken (supporting again records when	herbelin
2010-01-12	Added module sharing support for typeclasses and hints (pri_auto_tactic).	soubiran
2010-01-12	revert commit 12650 for the moment, since it breaks MSetAVL	letouzey
2010-01-12	Temporary fix to compensate the loss of descent on dependent	herbelin
2009-12-30	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin
2009-12-29	Improving descend_in_conjunctions (using a combinators instead of a tactic)	herbelin
2009-12-28	Safer, though ad hoc, approach to re-interpretation of the argument of	herbelin
2009-12-27	Fix "Existing Instance" to handle globality information and "Existing	msozeau
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-23	Moved a bit further the code for pattern interpretation in match goal	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-19	Backtrack on making exact hints for lemmas starting with products	msozeau
2009-12-16	adding an option functional_induction_rewrite_dependent to make functional in...	jforest
2009-12-14	Improved strategy for rewriting lemma possibly depending because of evars.	herbelin
2009-12-13	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin
2009-12-13	Completion of r12580 (better rendering of dependent rewrite and inversion).	herbelin
2009-12-13	Revision 12557 continued (better rendering of dependent rewrite)	herbelin
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-12-12	Improved the rendering of "dependent rewrite" and hence of "inversion"	herbelin
2009-12-06	Turn evars created by a tactic application into a subgoal immediately in	msozeau
2009-12-06	Fix anomaly when using typeclass resolution with filtered hyps in evars.	msozeau
2009-12-03	Restored rewriting of JMeq using JMeq_rect and co when the domains are the same	herbelin
2009-12-01	Fix make_exact_entry to allow applying [forall x, P x] hints directly,	msozeau
2009-12-01	Fix bug in typeclass resolution. Better handling of universes in	msozeau
2009-11-30	Fix backtracking heuristic in typeclass resolution.	msozeau
2009-11-27	Substitute terms for evars-as-goals as soon as they are solved in	msozeau
2009-11-24	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau
2009-11-21	Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...	puech
2009-11-12	Addendum to revision 12501.	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Backtracking on the use of automatically generated schemes for	herbelin
2009-11-10	Compatibility ocaml <= 3.09	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-09	Quick fix for restoring a left-to-right rewriting lemma compatible	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-11-06	- Fix discharge bug in typeclasses: some constrs were not actually	msozeau
2009-11-06	Misc fixes.	msozeau
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Clarification in comments	glondu