coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	New fix for is_ident_not_keyword.	herbelin	2011-08-13
*	Fixes mini-bug: Qed would succeed even on focused proofs.	aspiwack	2011-08-12
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	Fixing typos in comments	herbelin	2011-08-10
*	Improving error message about coinductive guard (old "cases" is now "match")	herbelin	2011-08-10
*	Fixing printing bug with last trailing non-maximally implicit	herbelin	2011-08-10
*	Exported tactic intro_then	herbelin	2011-08-10
*	Made CHANGES more uniformly written	herbelin	2011-08-10
*	Take benefit of bullets available by default in Prelude	herbelin	2011-08-10
*	Less ambitious application of a notation for eq_rect. We proposed	herbelin	2011-08-10
*	Partly revert commit r14389 about relaxing the condition for being a keyword	herbelin	2011-08-10
*	Fix implementation of Hint Immediate used by typeclasses eauto	msozeau	2011-08-10
*	Added list_map_filter_i	msozeau	2011-08-10
*	Graceful error message for [Proof Mode] and [Set Default Proof Mode] when req...	aspiwack	2011-08-10
*	BinInt: more structured scripts thanks to bullets and { }	letouzey	2011-08-09
*	Coqide: revised parsing of coq sentences	letouzey	2011-08-09
*	In coqtop, a terminating "." must now be followed by a blank or eof.	letouzey	2011-08-09
*	Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...	aspiwack	2011-08-09
*	Some forgotten lemma in Arith with "O" in the name instead of "0".	herbelin	2011-08-08
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	Be a bit less aggressive in declaring idents as keywords in notations	herbelin	2011-08-08
*	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