coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN	pboutill	2012-06-15
*	coq_makefile fixup	pboutill	2012-06-14
*	New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles	pboutill	2012-06-12
*	Fixing test-suite after last storm in Pp.	pboutill	2012-06-12
*	Getting rid of Pcoq remains.	ppedrot	2012-06-12
*	Colorization of coqtop messages is turned off by default	letouzey	2012-06-07
*	Fixing previous commit (something strange happened...)	ppedrot	2012-06-04
*	Replacing some str with strbrk	ppedrot	2012-06-04
*	Added a color output to Coqtop.	ppedrot	2012-06-04
*	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot	2012-06-04
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	Fixed printing error problem... A line had disappeared in a previous patch.	ppedrot	2012-06-02
*	Flushing formatters before program exit.	ppedrot	2012-06-02
*	More cleaning	ppedrot	2012-06-01
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Let's try to avoid generating induction principles for records (wish #2693)	letouzey	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	More uniformisation in Pp.warn functions.	ppedrot	2012-05-30
*	Re-allow Time Back* (cf discussion on coq-club)	letouzey	2012-05-29
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29
*	Avoid Dumpglob dependency on Lexer	letouzey	2012-05-29
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	Split Egrammar into Egramml and Egramcoq	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29
*	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey	2012-05-29
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29
*	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill	2012-05-23
*	Added a SearchAbout-like primitive in coqtop interface.	ppedrot	2012-05-13
*	Added an interface primitive to ask coqtop for its internal versions.	ppedrot	2012-05-13
*	Slightly modified the coqtop interface by adding an identifier in	ppedrot	2012-05-11
*	Added an interface call to exit Coqtop nicely.	ppedrot	2012-05-02
*	Implicit arguments of Definition are taken from the type when given by the user.	pboutill	2012-04-27
*	migrate g_obligations.ml4 in parsing	letouzey	2012-04-26
*	Program: avoid staying in program mode after a failed Program command	letouzey	2012-04-26
*	correct abort in Function when a proof of inversion fails	letouzey	2012-04-23
*	Supporting optional byte-mark order in utf-8 files (bug #2757).	herbelin	2012-04-19
*	Corrects a (very) longstanding bug of tactics. As is were, tactic expecting	aspiwack	2012-04-18
*	Bug 2733 : { } implicits and Fixpoints	pboutill	2012-04-17
*	Better error message when defining recursive records with Record or	aspiwack	2012-04-13
*	Remove print call that do not use the pp mechanism	pboutill	2012-04-12
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Relax uniform inheritance condition	gareuselesinge	2012-04-05
*	Added a command "Unfocused" which returns an error when the proof is	aspiwack	2012-03-30