coq - The formal proof system

Age	Commit message (Expand)	Author
2012-07-11	Also allow Reset in Load'ed files	letouzey
2012-07-11	Re-allow Reset in compiled files	letouzey
2012-07-11	Severe reorganisation of the code of tactics in Proofview.	aspiwack
2012-07-11	Fix regression introduced in r15418 that broke MathClasses. In program mode, ...	msozeau
2012-07-11	Fix typeclass error handling which was sometimes raising a Failure ("hd").	msozeau
2012-07-11	A friendlier printing of remaining goals when no goal is focused.	aspiwack
2012-07-10	Fixing Print Assumption display	ppedrot
2012-07-10	Restore test file induct.v where the "in \|- *" is mandatory	letouzey
2012-07-10	isolate instances about Permutation and PermutationA which may slow rewrite	letouzey
2012-07-10	Better treatment of error messages in rewrite (avoid use of Errors.print).	msozeau
2012-07-10	Adapting the IDE interface with the focussed display.	ppedrot
2012-07-10	Small change in the printing of proofs for use by coqide.	aspiwack
2012-07-10	Fixes bug 2841 ([Focus 0] gives anomaly).	aspiwack
2012-07-10	Another correction to the dependent existential variable printing	aspiwack
2012-07-09	destruct: full compatibility with former _eqn syntax	letouzey
2012-07-09	Moved code out of ide_slave in a more appropriate place.	ppedrot
2012-07-09	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-08	verbose compat notations : nicer option name	letouzey
2012-07-07	Restore an indentation of Show Script	letouzey
2012-07-07	Ring_polynom : a restricted simpl instead of a unfold;fold	letouzey
2012-07-06	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-05	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-04	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