coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2010-03-06	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau
2010-03-05	Minor fixes.	msozeau
2010-02-12	Delineating a API for Coq inside toplevel/vernac.ml	vgross
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
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-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2010-01-02	Fix bug in last commit, missing a substitution call.	msozeau
2010-01-01	Fix handling of instance declarations in presence of let-ins (bug	msozeau
2009-12-27	Fix "Existing Instance" to handle globality information and "Existing	msozeau
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-13	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin
2009-12-12	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin
2009-12-12	Updated compatibility for rewriting equality proofs that are dependent	herbelin
2009-12-08	Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...	letouzey
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-25	Fix for notation scope & inductive types	vsiles
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