coq - The formal proof system

Age	Commit message (Expand)	Author
2010-10-31	An experimental support for open constrs in hints and in "using"	herbelin
2010-10-05	Auto-inlining of f_terminate in Function	jforest
2010-09-30	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu
2010-09-28	Remove some occurrences of "open Termops"	glondu
2010-09-28	Remove "init" label from Termops.it_mk* specialized functions	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-21	Report fix bug 2345 from v8.3 (Bad error message when functional	courtieu
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-23	correcting a bug in funind introduced in r 13292	jforest
2010-07-22	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin
2010-07-16	Amelioration dans Function	jforest
2010-06-30	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau
2010-06-29	change the flag "internal" in declare/ind_tables from bool to	vsiles
2010-06-14	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-09	Allowing to use an ordering different than Lt with measure	jforest
2010-06-08	Using vernac parsing for Function	jforest
2010-05-19	Remove compile-command pragmas for emacs	letouzey
2010-05-07	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-04	Correction of bug 2290 (removing stupid message)	jforest
2010-05-04	Correction of bug 2290	jforest
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2010-03-12	fixed confusion between number of cstr arguments and number of pattern variab...	barras
2010-03-01	amelioration mineure dans Function	jforest
2010-02-24	correction of bug #2088	jforest
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-16	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-12	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-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
2009-12-02	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin
2009-12-01	Continuing r12485-12486 (cleaning around name generation)	herbelin
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
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-11-03	OrderedType implementation for various numerical datatypes + min/max structures	letouzey
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-03	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
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