coq - The formal proof system

Age	Commit message (Expand)	Author
2012-07-21	Fixing unchecked overflow in sub_mult used for euclidian division over	herbelin
2012-07-21	Slight modification to the printing of goals when in emacs mode.	courtieu
2012-07-20	Reductionops refactoring	pboutill
2012-07-20	Fixup implicits in patterns & notations	pboutill
2012-07-20	Vector equalities first stuff	pboutill
2012-07-20	Put Option in Clib	pboutill
2012-07-20	Fixing test-suite	pboutill
2012-07-20	Let coqtop be a little more stupid in hint answer: otherwise, that	ppedrot
2012-07-19	Getting rid of the undocumented [complete] tactic, which was	ppedrot
2012-07-18	Various minor fixes to coqdoc from A. Chlipala.	msozeau
2012-07-16	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-13	Display the "unjustified" information returned by coqtop.	ppedrot
2012-07-13	Fixes r15610 (A new status Unsafe in Interface).	aspiwack
2012-07-12	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-11	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-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