coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-15	Document Generalizable Variables, and change syntax to	msozeau
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-06	Misc fixes.	msozeau
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Module type expressions of the form (Fsig X) with Definition foo := bar are n...	soubiran
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-10-25	Restore (and test) broken chaining of lemmas in "apply in" in presence	herbelin
2009-10-25	fixed bug in Czar grammar	corbinea
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-04	Removal of trailing spaces.	serpyc
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-27	Complement to 12347 and 12348 on the extended syntax of case/elim.	herbelin
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-20	Add "case as/in/using" and temporary "destruct" with n args.	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-14	- Addition of "Reserved Infix" continued.	herbelin
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-09-10	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin
2009-09-02	Postpone checking of Local/Global to allow grammar extensions to use it	msozeau
2009-08-14	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack
2009-08-14	Added profile.cmo in grammar.cma so that any functions in one of the	herbelin
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-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-07-15	- Granted wish #2138 (support for local binders in syntax of Record fields).	herbelin
2009-06-29	Miscellaneous practical commits:	herbelin
2009-06-15	Allow anonymous instances again, with syntax [Instance: T] where T	msozeau
2009-06-11	Simplifying the call to print_no_goals and not calling it when no goal	herbelin
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-06-03	Ensure the precondition of the partial function [list_chop] holds	msozeau
2009-05-28	Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonction	aspiwack
2009-05-27	Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dans	aspiwack
2009-05-27	=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...	aspiwack
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-27	- Fixed a little bug in previous commit (bad failure in case of unknown entry).	herbelin
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-04-08	Some dead code removal + cleanups	letouzey