coq - The formal proof system

Age	Commit message (Expand)	Author
2010-01-28	Fix implicit_application for let-bound variables in the class context.	msozeau
2010-01-28	Backport fixes in Instance declarations to Program Instance.	msozeau
2010-01-17	Variant !F M for functor application that does not honor the Inline declarations	letouzey
2010-01-07	Include can accept both Module and Module Type	letouzey
2010-01-06	Allowed handling of partly-applied record constructors. (Fix for bug #2196.)	gmelquio
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-21	Generic support for open terms in tactics	herbelin
2009-12-19	Made the interpretation levels rlevel/glevel/tlevel truly phantom	herbelin
2009-12-13	Deactivating printing of {\| \|} for records when option Printing All is set.	herbelin
2009-12-12	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin
2009-12-07	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-18	Module subtyping : allow many <: and module type declaration with <:	letouzey
2009-11-16	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey
2009-11-12	Experiment propagation of implicit arguments and arguments scope for	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-09	Deactivation of (intrusive) printing of abbreviations from non-imported modules.	herbelin
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-08	Use generalizable variables info when internalizing arbitrary bindings,	msozeau
2009-11-06	Misc fixes.	msozeau
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-11-02	list, length, app are migrated from List to Datatypes	letouzey
2009-10-29	Revision 12439 continued, printing part (notations to names behave	herbelin
2009-10-28	Made that notations to names behave like the names they refer to wrt	herbelin
2009-10-28	Fixed a bug when reporting unexisting reference to an inductive	herbelin
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-26	Local/Global revision 12418 continued	herbelin
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-17	Fixed a notation bug when extending binder_constr with empty levels	herbelin
2009-10-09	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau
2009-09-27	Fixed error message "cannot infer the type of id" in presence of	herbelin
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-22	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-06-07	- Added two new introduction patterns with the following temptative syntaxes:	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-30	Fix a small notation/scope bug:	vsiles
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-08	Some dead code removal + cleanups	letouzey