coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-28	Remove old compatibility stuff (Tacred.nf)	glondu
2009-10-28	Make usage of Dyn explicit	glondu
2009-10-28	Backport fix for indexing of sorts which collapse every Type occurrence	msozeau
2009-10-27	Fixes around typeclasses:	msozeau
2009-10-27	fix previous commit	corbinea
2009-10-27	fixed czar bug with parametric inductives	corbinea
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	Add support for remaining side-conditions in "apply in as".	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-24	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin
2009-10-23	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-15	Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:	msozeau
2009-10-06	Relaxed error severity when encountering unknown library objects or tactic	gmelquio
2009-10-05	Correctly do backtracking during type class resolution even if only new	msozeau
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	Remove legacy export_* functions	glondu
2009-09-27	Apply "Declare Implicit Tactic" also to terms interpreted as "open	herbelin
2009-09-27	Fixed a bug in the interaction between dEqThen and inject_at_positions	herbelin
2009-09-27	Delay the choice of eliminator in destruct/induction until we know if	herbelin
2009-09-26	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin
2009-09-22	Better use of transparency information for local hypotheses:	msozeau
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-18	- Fixed a bug in checking that implicit arguments are all correctly	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-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-09	Allow setoid rewrite to rewrite in pattern-matching scrutinees or	msozeau
2009-09-09	Stop trying to search if the relation is declared as a [RewriteRelation]	msozeau
2009-09-08	Fix the bug-ridden code used to choose leibniz or generalized	msozeau
2009-09-03	Support globality flag properly for "Add Morphism foo : foo_mor" syntax.	msozeau
2009-09-02	Stop unnecessary use of lazy values for constraints, simplifying	msozeau
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-06	Move out JMeq of subst for compatibility (it affects e.g. the	herbelin
2009-08-04	- Add more precise error localisation when one of the application fails	herbelin
2009-08-04	Fixed subst failing when a truly heterogeneous JMeq hyp is in the	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-08-02	Fixed a typo in "info" for tactic "right".	herbelin
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-07-14	Simplify eauto and fix it for compatibility, allowing full delta during	msozeau
2009-07-09	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau
2009-07-08	Simplify addition of hints to a hint_db. Rebuild the dnet associated	msozeau
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin