coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-18	Now "Include Self <expr>" handles partially applied functors, cf for example ...	soubiran
2009-11-18	Allow interactive proofs in module types	letouzey
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-16	Include Self (Type) Foo: applying a (Type) Functor to the current context	letouzey
2009-11-15	Fix [Instance: forall ..., C args := t] declarations to behave as	msozeau
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	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	Fixed "Scheme Equality" when another instance of the scheme on the	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-29	Hopefully improved layout of fix guardness error message.	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-27	Documentation of the Local and Global modifiers.	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-16	note for later : when the tag table is shared, never, ever create two	vgross
2009-10-13	MSets: a new generation of FSets	letouzey
2009-10-09	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau
2009-10-05	Correctly do backtracking during type class resolution even if only new	msozeau
2009-10-05	Revert "kills the old backtracking framework and replaces it with"	vgross
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-29	Add support for Local Declare ML Module	glondu
2009-09-29	Remove legacy export_* functions	glondu
2009-09-29	kills the old backtracking framework and replaces it with	vgross
2009-09-26	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin
2009-09-22	Add the option to automatically introduce variables declared before the	msozeau
2009-09-17	Replace call to where_in_path by find_file_in_path in "Locate File"	glondu
2009-09-17	Replace unprotected call to where_in_path by find_file_in_path	glondu
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-15	Fixed compilation error message which was no longer emacs-compliant since	herbelin
2009-09-14	Backtrack on the forced discharge of type class variables introduced	msozeau
2009-09-14	- Addition of "Reserved Infix" continued.	herbelin
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-09-02	Postpone checking of Local/Global to allow grammar extensions to use it	msozeau
2009-09-02	Stop unnecessary use of lazy values for constraints, simplifying	msozeau
2009-08-14	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-11	Add support for "Infix ... := constr" instead of just "Infix ... := ref".	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