coq - The formal proof system

Age	Commit message (Expand)	Author
2012-07-29	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin
2012-07-25	documentation of bullets (forward port from v8.4).	courtieu
2012-07-25	Fix eta contraction in Reductionops	pboutill
2012-07-25	Bug 2706: Coqide and layout that use special modifiers	pboutill
2012-07-25	Same for Fin	pboutill
2012-07-21	Fixing bug #2835 (the rationale for printing notations was not	herbelin
2012-07-21	Improving management of notations with binders (see #2708 where a	herbelin
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