coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Term	puech	2011-07-29
*	Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...	puech	2011-07-29
*	Newring: generic equality on constr replaced by constr_equal	puech	2011-07-29
*	Ccproof: generic equality on term replaced by term_equal	puech	2011-07-29
*	Sequent: generic equality on global_reference replaced by RefOrdered.compare	puech	2011-07-29
*	Sequent: generic equality on kernel_name replaced by kn_ord	puech	2011-07-29
*	Sequent: generic equality on constr replaced by destructors	puech	2011-07-29
*	Sequent: generic equality on ident replaced by id_ord	puech	2011-07-29
*	Instances: generic equality on global_reference replaced by RefOrdered.compare	puech	2011-07-29
*	Unify: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Integral domains	pottier	2011-07-26
*	Ring2 devient Ncring et la reification par les type classes est partagee	pottier	2011-07-26
*	Add a syntax entry for fully applied constructor pattern	pboutill	2011-07-22
*	Set Extraction KeepSingleton: an option for not decapsulating singleton types	letouzey	2011-07-04
*	Extraction: in haskell, __ may have any type, no need to unsafeCoerce it	letouzey	2011-07-04
*	Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)	letouzey	2011-07-04
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Fix compilation error	msozeau	2011-06-30
*	Keep obligation source information in Program	msozeau	2011-06-30
*	update of Micromega doc	fbesson	2011-06-29
*	Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def	letouzey	2011-06-28
*	improved tactic names	fbesson	2011-06-28
*	Numbers: a particular case of div_unique	letouzey	2011-06-24
*	Follow-up concerning eqb / ltb / leb comparisons	letouzey	2011-06-21