coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	A new status Unsafe in Interface. Meant for commands such as Admitted.	aspiwack	2012-07-12
*	Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)	letouzey	2012-07-12
*	Ensure that a plugin init function is called only once	letouzey	2012-07-12
*	Vernacentries: minor code cleanup	letouzey	2012-07-12
*	Bug 2838: ExplApp in mutual inductive parameters	pboutill	2012-07-12
*	Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfind	pboutill	2012-07-12
*	Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820	letouzey	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-11
*	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-10
*	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-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