coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Extraction: replace generic = on mutual_inductive_body by mib_equal	puech	2011-07-29
*	Evarutil: replace generic list_distinct on constr by constr_list_distinct	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
*	Add printer dependency to Hashtbl_alt (used in Term)	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
*	Evarutil: replaced some generic = on constr by destructors	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
*	Hahtbl_alt: separate generic combine functions	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
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Class_tactics: generic equality on named_context_val replaced by eq_named_con...	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
*	Eqschemes: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by destructors	puech	2011-07-29
*	Heads: generic equality on constr replaced by destructor	puech	2011-07-29
*	Environ: generic equality on named_context replaced by named_context_equal	puech	2011-07-29
*	Evarconv: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Equality: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Cases: generic equality on constr replaced by destructors	puech	2011-07-29
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Classops: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Class: generic equality on constr replaced by destructors	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr (x2)	puech	2011-07-29
*	Equality: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tactics: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tactics: generic equality on named_declaration replaced by eq_named_declaration	puech	2011-07-29
*	Term: added function eq_named_declaration	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Tacred: generic equality on constr replaced by eq_constr	puech	2011-07-29