coq - The formal proof system

Age	Commit message (Expand)	Author
2010-01-30	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau
2010-01-12	New version of 12650 that was broken (supporting again records when	herbelin
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-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-13	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin
2009-12-01	Fix bug in typeclass resolution. Better handling of universes in	msozeau
2009-11-24	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	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-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-25	Restore (and test) broken chaining of lemmas in "apply in" in presence	herbelin
2009-10-25	Add support for remaining side-conditions in "apply in as".	herbelin
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-10-04	Removal of trailing spaces.	serpyc
2009-10-03	Added option "Unset Dependent Propositions Elimination" to protect	herbelin
2009-09-27	Delay the choice of eliminator in destruct/induction until we know if	herbelin
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-18	- Fixed a bug in checking that implicit arguments are all correctly	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-10	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-04	- Add more precise error localisation when one of the application fails	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-16	Reimplementation of leibniz rewrite to control the instantiation of the	msozeau
2009-06-07	- Added two new introduction patterns with the following temptative syntaxes:	herbelin
2009-06-06	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin
2009-05-18	Minor unification changes:	msozeau
2009-05-17	- Allowing multiple calls to tactic fix with automatic generation of	herbelin
2009-04-24	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin
2009-04-10	Fix premature optimisation in dependent induction: even variable args need	msozeau
2009-03-31	Fix auto so that Extern tactics associated to no patterns can apply to	msozeau
2009-03-22	Compromise wrt introduction-names compatibility issue after addition	herbelin
2009-03-17	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-02-23	Add support for dependent "destruct" over terms in dependent types.	herbelin
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-16	Fix [apply_in] which short-circuited resolution of evars in a custom	msozeau
2009-02-06	pushed evar reduction in kernel	barras
2009-02-04	Report r11631 from 8.2 and handle non-dependent goals better in	msozeau
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin