coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Win32: some quote fixes	letouzey	2012-08-06
*	MSetRBT: a tail-recursive plength	letouzey	2012-08-06
*	Try to make the use of Unix.lockf in micromega compatible with Win32	letouzey	2012-08-06
*	Dump references in Extraction	pboutill	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-05
*	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-03
*	Bigint: new functions of_int and to_int, 2nd arg of pow in int	letouzey	2012-08-02
*	Bigint: adds a missing -1 in hugo's last commit 15659	letouzey	2012-07-31
*	Bigint : better ensure canonicity of arrays of int blocks	letouzey	2012-07-30
*	Bigint: avoid dependency over Pp	letouzey	2012-07-30
*	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-29
*	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-25
*	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-21
*	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-20
*	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