coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-08-02	Improved parameterization of Coq:	herbelin
2009-07-08	Use user-given implicits from the arity in inductive definitions.	msozeau
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-07-01	Support for binding Coq root read-only in -R option	herbelin
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-06-18	Fix "unsatisfiable constraints" error messages to include all the	msozeau
2009-06-13	Correct typo: -noglob takes no argument.	msozeau
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-05-27	Fix implicit args code so that declarations are added for all	msozeau
2009-05-27	Stop using a "Manual Implicit Arguments" flag and support them as soon	msozeau
2009-05-16	Minor fixes in typeclasses:	msozeau
2009-05-13	Fix to my last notation patch: now fixpoint are correctly handled	vsiles
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	- 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