coq - The formal proof system

Age	Commit message (Expand)	Author
2011-09-01	Coq_makefile: New option -arg to specify a compiler option.	pboutill
2011-09-01	Coq_makefile drops the '/' at the end of physical path of -I and -R	pboutill
2011-09-01	Several bug reports came from confusions between generalize and set.	pboutill
2011-09-01	Bug 2583: Update of the syntax of terms in the reference manual	pboutill
2011-09-01	Bug 2577: Second attempt to be correct.	pboutill
2011-08-30	Porting Hendrik's 8.3 patch for proof tree visualization under proof	herbelin
2011-08-30	Quick improvement of some error messages related to module application	herbelin
2011-08-25	Extraction: allow extraction of records with anonymous fields (fix #2555)	letouzey
2011-08-23	Use of the standard terminology for Diaconescu's theorem (not "paradox").	herbelin
2011-08-23	Clarifying that only identifiers are advertised to be turned into keywords	herbelin
2011-08-22	Tactics.compute_scheme_signature: factorize the two almost-similar cases	letouzey
2011-08-18	Updates in CHANGES	letouzey
2011-08-18	Remove old file (1999)	msozeau
2011-08-18	Misc improvements concerning "Show Match" and its coqide equivalent	letouzey
2011-08-17	Give inner fixpoint of gcd31 a name, to avoid excessive unfolding	glondu
2011-08-17	Smaller proof terms for QcPower_{0,pos}	glondu
2011-08-16	Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)	aspiwack
2011-08-13	New fix for is_ident_not_keyword.	herbelin
2011-08-12	Fixes mini-bug: Qed would succeed even on focused proofs.	aspiwack
2011-08-11	SearchAbout and similar: add a customizable blacklist	letouzey
2011-08-10	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-09	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-08	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-04	moins de reification inutile, noatations standards	pottier
2011-08-04	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau
2011-08-03	Fix nf_evars_undefined use in pr_constraints	msozeau
2011-08-03	Fix nf_evars_undefined	msozeau
2011-08-02	Patch to simplify is_open_canonical_projection	herbelin
2011-08-02	More robust evar_map debugging printer	herbelin
2011-08-01	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