coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Getting rid of the undocumented [complete] tactic, which was	ppedrot	2012-07-19
*	Various minor fixes to coqdoc from A. Chlipala.	msozeau	2012-07-18
*	Added abstration layer to goal display in CoqIDE, and cleaned parts	ppedrot	2012-07-16
*	Fixing goal display when still focussing but no more goals.	ppedrot	2012-07-16
*	Display the "unjustified" information returned by coqtop.	ppedrot	2012-07-13
*	Fixes r15610 (A new status Unsafe in Interface).	aspiwack	2012-07-13
*	flex_maybeflex factoring	pboutill	2012-07-12
*	miller_pfenning unification code factoring	pboutill	2012-07-12
*	flex_kind_of_term does not have a copy of term	pboutill	2012-07-12
*	evar reduction is already made by whd_*	pboutill	2012-07-12
*	tacred uses stack_reduction_function instead of state_reduction_function	pboutill	2012-07-12
*	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