coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-01-03	Fixed two problems:	herbelin
2009-01-02	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin
2008-12-18	- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a side	herbelin
2008-12-16	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau
2008-12-12	Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...	herbelin
2008-12-09	About "apply in":	herbelin
2008-11-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
2008-11-05	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau
2008-10-29	Adaptation du vieil appel à "apply" sur lemme de symétrie au cas où	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin