coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Look for csdp in $PATH at runtime, remove -csdpdir configure option	glondu	2010-04-11
*	Remove unused functions run_sdpa	glondu	2010-04-11
*	Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using i...	letouzey	2010-03-30
*	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
*	Application des patches envoyés par F. Besson pour micromega	notin	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
*	Improvements in generalized rewriting:	msozeau	2010-03-05
*	Add a generic tactic option builder. Use it in firstorder to set the	msozeau	2010-03-05
*	amelioration mineure dans Function	jforest	2010-03-01
*	Win32 cross-compilation from debian: build of coqide.exe and other binaries	letouzey	2010-02-24
*	correction of bug #2088	jforest	2010-02-24
*	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