coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix sort_dependencies for good, maintaining the initial order.	msozeau	2010-02-16
*	bug in field_simplify_eq in	barras	2010-02-10
*	Euclidean division for NArith	letouzey	2010-02-10
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	New command Declare Reduction <id> := <conv_expr>.	letouzey	2010-01-28
*	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
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24
*	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
*	Const_omega: look for S in Init only (avoid future clash with S of Numbers)	letouzey	2009-12-18
*	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
*	Fix the build of coq via ocamlbuild	letouzey	2009-12-08
*	Sos.ml: no more warnings	letouzey	2009-12-08
*	Continuing r12485-12486 and r12549 (cleaning around name generation)	herbelin	2009-12-02
*	Remove interface plugin	glondu	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
*	Fixing xml theory file export (was not consistent with coqdoc file	herbelin	2009-11-26
*	Module subtyping : allow many <: and module type declaration with <:	letouzey	2009-11-18
*	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey	2009-11-16
*	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
*	Repair interpretation of numeral for BigQ, add a printer (close #2160)	letouzey	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
*	use only why-dp, support for z3	marche	2009-11-10
*	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
*	Make usage of Dyn explicit	glondu	2009-10-28
*	Add a new vernacular command for controling implicit generalization of	msozeau	2009-10-27
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	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
*	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey	2009-10-08
*	Fix for missing hypotesae in XML proof tree export.	cek	2009-10-07
*	Removal of trailing spaces.	serpyc	2009-10-04
*	Fixed small name freshness bug in Functional Scheme ("Heq" name was	herbelin	2009-10-03