coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin	2011-11-17
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Bug 2636 - Move string_of_ppcmds to Pp	pboutill	2011-11-14
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Remove avoidable use of GDynamic	glondu	2011-10-27
*	Fixing Equality.injectable which did not detect an equality without	herbelin	2011-10-22
*	Fix bug #2227	msozeau	2011-10-18
*	Fix inductive coercion code in Program (bug #2378)	msozeau	2011-10-18
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Fix bug #2557 and an issue with Propers for complement	msozeau	2011-10-07
*	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin	2011-10-05
*	In Coq_config: get rid of coqsrc and make coqlib optional	glondu	2011-09-27
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Generalizing subst_term_occ so that it supports an arbitrary matching	herbelin	2011-09-26
*	Fix commit 14489: missing Coq. in dirpath	letouzey	2011-09-23
*	Program: add some check_required_library (fix #2592) + some dead code removal	letouzey	2011-09-23
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16
*	Omega aware of Z.pred (fix #1912)	letouzey	2011-09-15
*	correction du bug 2047	jforest	2011-09-09
*	Improved ltac code for zify (fix #2575).	letouzey	2011-09-06
*	Extraction Implicit: fix the numbering of constructor arguments	letouzey	2011-09-05
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
*	Extraction: allow extraction of records with anonymous fields (fix #2555)	letouzey	2011-08-25
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	moins de reification inutile, noatations standards	pottier	2011-08-04
*	Ring: replaced various generic = on constr by eq_constr, destructors etc.	puech	2011-07-29
*	Quote: replaced various generic = on constr by eq_constr, destructors etc.	puech	2011-07-29
*	Newring: generic = on constr replaced by eq_constr	puech	2011-07-29
*	Coq_micromega: generic = on constr replaced by eq_constr	puech	2011-07-29
*	Field: generic Gmap on constr replaced by Cmap	puech	2011-07-29
*	Extract_env: generic = on prec_declaration replaced by prec_declaration_equal	puech	2011-07-29
*	Extraction: replace generic = on mutual_inductive_body by mib_equal	puech	2011-07-29
*	replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Subtac_cases: replaced some generic = on constr by destructors	puech	2011-07-29
*	Ring: replaced some generic Pervasives.compare on constr by constr_ord	puech	2011-07-29
*	Nsatz: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Recdef: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	FourierR: replaced some generic Hashtbl on constr by Constrhash	puech	2011-07-29
*	Refl_omega: replaced generic = on constr by eq_constr	puech	2011-07-29
*	Newring: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Refl_omega: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Const_omega: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Functional_principles_types: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Newring: replaced generic = on constr by eq_constr	puech	2011-07-29
*	Coq_omega: replaced generic = on constr by eq_constr	puech	2011-07-29
*	Quote: replaced generic = on constr by eq_constr	puech	2011-07-29
*	Coq_omega: replaced many generic = on constr by eq_constr	puech	2011-07-29
*	Newring: generic Pervasives.compare on constr replaced by constr_ord	puech	2011-07-29