coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	Fix bug 2269, program typechecker not used in Instance conclusions	msozeau	2011-06-17
*	Tests de nsatz avec la geometrie	pottier	2011-06-16
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Call process_vernac_interp_error before calling Errors.print in	herbelin	2011-06-10
*	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill	2011-06-10
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
*	Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...	msozeau	2011-06-07
*	Fix bug #2415: warn when closing modules or sections and some obligations are...	msozeau	2011-06-07