coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Oops, don't use zeta by default.	msozeau	2010-03-15
*	Fix splitting evars tactics and stop dropping evar constraints when	msozeau	2010-03-15
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	Consider OccurCheck a catchable exception.	msozeau	2010-03-08
*	Reorder resolution of type class and unification constraints.	msozeau	2010-03-07
*	Fix treatment of remaining unification constraints: raise a more	msozeau	2010-03-07
*	Add a generic tactic option builder. Use it in firstorder to set the	msozeau	2010-03-05
*	Fix sort_dependencies for good, maintaining the initial order.	msozeau	2010-02-16
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	Backport fixes in Instance declarations to Program Instance.	msozeau	2010-01-28
*	Add [Next Obligation with tactic] support (wish #1953).	msozeau	2010-01-26
*	Fix bug #2086, error message when we match on an non-inductive type.	msozeau	2010-01-14
*	- Show Obligation Tactic	msozeau	2010-01-14
*	Support "Local Obligation Tactic" (now the default in sections).	msozeau	2010-01-11
*	Specific syntax for Instances in Module Type: Declare Instance	letouzey	2010-01-04
*	Few misc. updates.	herbelin	2010-01-04
*	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin	2009-12-24
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	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-12
*	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