coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	correcting a bug in funind introduced in r 13292	jforest	2010-07-23
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	Amelioration dans Function	jforest	2010-07-16
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	change the flag "internal" in declare/ind_tables from bool to	vsiles	2010-06-29
*	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin	2010-06-14
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Allowing to use an ordering different than Lt with measure	jforest	2010-06-09
*	Using vernac parsing for Function	jforest	2010-06-08
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	better detection of nested recursion in Function	jforest	2010-05-07
*	Correction of a bug pointed by P. Casteran.	jforest	2010-05-07
*	Trying to find a problem pointed by P. Casteran	jforest	2010-05-07
*	Correction of bug 2290 (removing stupid message)	jforest	2010-05-04
*	Correction of bug 2290	jforest	2010-05-04
*	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
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	amelioration mineure dans Function	jforest	2010-03-01
*	correction of bug #2088	jforest	2010-02-24
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	correction de la nouvelle option pour functional induction	jforest	2009-12-16
*	adding an option functional_induction_rewrite_dependent to make functional in...	jforest	2009-12-16
*	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin	2009-12-12
*	Updated compatibility for rewriting equality proofs that are dependent	herbelin	2009-12-12
*	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey	2009-12-09
*	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin	2009-12-02
*	Continuing r12485-12486 (cleaning around name generation)	herbelin	2009-12-01
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	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
*	OrderedType implementation for various numerical datatypes + min/max structures	letouzey	2009-11-03
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin	2009-10-03
*	Remove useless Liboject.export_function field	glondu	2009-09-17
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	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
*	repport of commit r12221	jforest	2009-07-04
*	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