coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Make usage of Dyn explicit	glondu	2009-10-28
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau	2009-10-09
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	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-15
*	Backtrack on the forced discharge of type class variables introduced	msozeau	2009-09-14
*	- Resolve type class constraints before trying to find unresolved	msozeau	2009-09-11
*	Misc fixes:	msozeau	2009-09-10
*	Hack to correctly get ill-formed rec body exceptions even	msozeau	2009-09-02
*	Death of "survive_module" and "survive_section" (the first one was	herbelin	2009-08-13
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	Fix bug introduced by last revision, subtac_cases was returning the	msozeau	2009-06-29
*	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-28
*	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau	2009-06-22
*	Use more consistent resolution parameters in Program and regular typing	msozeau	2009-06-18
*	Fallback on not using [fix_proto] if the right imports aren't there, the	msozeau	2009-06-17
*	Use a lazy value for the message in FailError, so that it won't be	msozeau	2009-06-11
*	Fix implicit args code so that declarations are added for all	msozeau	2009-05-27
*	Fix de Bruijn lifting bug appearing when we match on multiple terms with	msozeau	2009-05-26
*	Support for definition hooks in subtac.	msozeau	2009-05-16
*	More efficient handling of evars in Program Fixpoint commands.	msozeau	2009-04-28
*	Backporting 12080 (fixing bug #2091 on bad rollback in the "where"	herbelin	2009-04-24
*	- New cleaning phase for the entry points of pretyping.ml	herbelin	2009-04-24
*	Better Requires in Classes. Fix bug #2093: the code does not require	msozeau	2009-04-16
*	Experimental support for automatic destruction of recursive calls and	msozeau	2009-04-08
*	Fix bug #2083 for good: verify that the measure and relation are	msozeau	2009-04-08
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	Fixes in Program:	msozeau	2009-04-07
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Fixes in Program well-founded definitions:	msozeau	2009-03-26
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20