coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Two bugs in pattern-matching compilation:	herbelin	2011-08-08
*	Term: fix hash_constr to hash modulo casts & names (like compare_constr)	puech	2011-08-08
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	moins de reification inutile, noatations standards	pottier	2011-08-04
*	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau	2011-08-04
*	Fix nf_evars_undefined use in pr_constraints	msozeau	2011-08-03
*	Fix nf_evars_undefined	msozeau	2011-08-03
*	Patch to simplify is_open_canonical_projection	herbelin	2011-08-02
*	More robust evar_map debugging printer	herbelin	2011-08-02
*	Term: simplify compare_constr by removing calls to decompose_app	puech	2011-08-01
*	Added .dir-locals file to take advantage of emacs 23's new Directory-local va...	puech	2011-08-01
*	fixed bug 2580. Quick fix: copy emitcodes before patching it	barras	2011-08-01
*	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
*	generic = on named_context replaced by named_context_equal	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
*	Tactics: replace generic = on constr by destructors	puech	2011-07-29
*	Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ord	puech	2011-07-29
*	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