coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	The tactic remember now accepts a final eqn:H option (grant wish #2489)	letouzey	2012-07-09
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Avoid a warning about unprintable new command Print Namespace	letouzey	2012-07-09
*	Fixed fake_ide test-suite.	ppedrot	2012-07-09
*	verbose compat notations : nicer option name	letouzey	2012-07-08
*	Restore an indentation of Show Script	letouzey	2012-07-07
*	Ring_polynom : a restricted simpl instead of a unfold;fold	letouzey	2012-07-07
*	Continuing r15459: it helps testing occur-check early in some	herbelin	2012-07-06
*	Minor fixes in the test-suite after my recent commits	letouzey	2012-07-06
*	Two adaptations after the changes of level of ->	letouzey	2012-07-06
*	BinPos/BinInt/BinNat : fix some argument scopes	letouzey	2012-07-06
*	Restore the compatibility notation Compare.not_eq_sym	letouzey	2012-07-06
*	Fix order of introduction of hints to preserve most-recent-first semantics.	msozeau	2012-07-06
*	A prototype implementation of a Print Namespace command.	aspiwack	2012-07-06
*	Fixes a bug in the parsing of the grammar entry dirpath which would,	aspiwack	2012-07-06
*	Practical fix for bug #1206 (anomaly raised in pretyping instead of	herbelin	2012-07-06
*	Fixes bug #2678	aspiwack	2012-07-06
*	Backtrack: add support for the "Proof c." syntax (fix #2832)	letouzey	2012-07-06
*	Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)	letouzey	2012-07-05
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	Quick update to CHANGES, mention especially the new parsing of ->	letouzey	2012-07-05
*	rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite	letouzey	2012-07-05
*	More cleanup in Ring_polynom and EnvRing	letouzey	2012-07-05
*	Some cleanup in recent proofs concerning pi	letouzey	2012-07-05
*	MSetRBT : elementary arith proofs instead of calls to lia	letouzey	2012-07-05
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	Open Scope can now also accepts delimiters (e.g. Z).	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Fixes in rewriting by strategies (almost ready to be documented!):	msozeau	2012-07-05
*	Fixes a bug in Ppvernac which had braces and bullets printed with an ending	aspiwack	2012-07-04
*	Change how the number of open goals is printed.	aspiwack	2012-07-04
*	When focused on an empty list of goal (after finishing a subproof introduced	aspiwack	2012-07-04
*	Various small display improvement	ppedrot	2012-06-29
*	Reversed message display order in CoqIDE	ppedrot	2012-06-29
*	Small improvement to ide_slave, which was going crazy whenever	ppedrot	2012-06-29
*	Fixing fake_ide	ppedrot	2012-06-29
*	Now CoqIDE separates answer and messages. This should hopefully	ppedrot	2012-06-29
*	Cleaning opening of the standard List module.	ppedrot	2012-06-28
*	Replace nat indices with positive one in Btauto.	ppedrot	2012-06-28
*	Fixing previous commit.	ppedrot	2012-06-28
*	Fixing info_auto / info_trivial display.	ppedrot	2012-06-28
*	Added the show_margin_right option to CoqIDE	ppedrot	2012-06-26
*	Fixing awkward copy & paste mechanism in CoqIDE.	ppedrot	2012-06-26
*	Now CoqIDE auto-sets the printing width of the goal display.	ppedrot	2012-06-26
*	Fixed string width printing in string_of_ppcmds	ppedrot	2012-06-26
*	Added a Deque module to CLib (to be used in CoqIDE).	ppedrot	2012-06-26
*	Small code compaction and factoring in CoqIDE.	ppedrot	2012-06-25
*	Added a .mli to pretyping/program.ml	ppedrot	2012-06-25