coq - The formal proof system

Age	Commit message (Expand)	Author
2012-08-05	Dump references in reduction tactics	pboutill
2012-08-05	Coqdoc: More keywords, better special char escape, special case for "in *"	pboutill
2012-08-05	Dump references	pboutill
2012-08-05	More entries in the index	pboutill
2012-08-05	Dump references in Reset	pboutill
2012-08-05	Revert "Fixing include printers"	pboutill
2012-08-03	Fixing include printers	ppedrot
2012-08-03	Document the command Add/Remove Search Blacklist	letouzey
2012-08-03	re-sync CHANGES with 8.4	letouzey
2012-08-02	Bigint: new functions of_int and to_int, 2nd arg of pow in int	letouzey
2012-07-31	Bigint: adds a missing -1 in hugo's last commit 15659	letouzey
2012-07-30	Bigint : better ensure canonicity of arrays of int blocks	letouzey
2012-07-30	Bigint: avoid dependency over Pp	letouzey
2012-07-29	Better fixing propagation of carry in sub_mult used for euclidian	herbelin
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