coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	same_file in Minilib	pboutill	2011-09-01
*	load_file takes advantage of same_file optimisation	pboutill	2011-09-01
*	create_session takes the filename as argument.	pboutill	2011-09-01
*	No more parser for reading coqide pref file	pboutill	2011-09-01
*	[/]+ is equivalent to [/] in System and its copy	pboutill	2011-09-01
*	Coq_makefile.absolute_dir -> Minilib.canonical_path_name	pboutill	2011-09-01
*	Creation of ide/project_file.ml4	pboutill	2011-09-01
*	gitignore update	pboutill	2011-09-01
*	Coq_makefile: Bug fix of check_dep	pboutill	2011-09-01
*	Coq_makefile: process_cmd_line is purely functional.	pboutill	2011-09-01
*	Coq_makefile: No other function than split_arguments uses a target type.	pboutill	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-09-01
*	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-30
*	Extraction: allow extraction of records with anonymous fields (fix #2555)	letouzey	2011-08-25
*	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-23
*	Tactics.compute_scheme_signature: factorize the two almost-similar cases	letouzey	2011-08-22
*	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-18
*	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-17
*	Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)	aspiwack	2011-08-16
*	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