coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-08	Consider OccurCheck a catchable exception.	msozeau
2010-03-07	Reorder resolution of type class and unification constraints.	msozeau
2010-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2010-03-05	Add a generic tactic option builder. Use it in firstorder to set the	msozeau
2010-02-16	Fix sort_dependencies for good, maintaining the initial order.	msozeau
2010-02-10	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau
2010-01-28	Backport fixes in Instance declarations to Program Instance.	msozeau
2010-01-26	Add [Next Obligation with tactic] support (wish #1953).	msozeau
2010-01-14	Fix bug #2086, error message when we match on an non-inductive type.	msozeau
2010-01-14	- Show Obligation Tactic	msozeau
2010-01-11	Support "Local Obligation Tactic" (now the default in sections).	msozeau
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2010-01-04	Few misc. updates.	herbelin
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-12	Oops, nf_evar_defs just changed to nf_evar_map.	msozeau
2009-11-12	Don't forget to normalize everything w.r.t. evars (fixes bug #2103).	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-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	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-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Make usage of Dyn explicit	glondu
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-09	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau
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	Dont't forget to update the state or an obligation tactic assignment may	msozeau
2009-09-15	Stop using [obligation_tactic] from Program.Tactics as the default	msozeau
2009-09-14	Backtrack on the forced discharge of type class variables introduced	msozeau
2009-09-11	- Resolve type class constraints before trying to find unresolved	msozeau
2009-09-10	Misc fixes:	msozeau
2009-09-02	Hack to correctly get ill-formed rec body exceptions even	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-02	Improved parameterization of Coq:	herbelin
2009-06-29	Fix bug introduced by last revision, subtac_cases was returning the	msozeau
2009-06-28	Abstract the tycon by the matched terms when turning them into variables	msozeau
2009-06-28	Improve return predicate inference by making the return type dependent	msozeau
2009-06-22	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-06-17	Fallback on not using [fix_proto] if the right imports aren't there, the	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-26	Fix de Bruijn lifting bug appearing when we match on multiple terms with	msozeau
2009-05-16	Support for definition hooks in subtac.	msozeau
2009-04-28	More efficient handling of evars in Program Fixpoint commands.	msozeau
2009-04-24	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin