coq - The formal proof system

Age	Commit message (Expand)	Author
2012-06-22	Fixing camlp4 compilation w.r.t previous commit	ppedrot
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-22	I forgot a line in previous commit.	aspiwack
2012-06-22	A call to the command Proof (and its variants) now prints the subgoals.	aspiwack
2012-06-21	Fix bug #2808: wrong handling of evars in Instance command.	msozeau
2012-06-15	Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN	pboutill
2012-06-14	coq_makefile fixup	pboutill
2012-06-12	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-07	Colorization of coqtop messages is turned off by default	letouzey
2012-06-04	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-02	Fixed printing error problem... A line had disappeared in a previous patch.	ppedrot
2012-06-02	Flushing formatters before program exit.	ppedrot
2012-06-01	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-05-30	Getting rid of Pp.msg	ppedrot
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
2012-05-29	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-23	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill
2012-05-13	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-11	Slightly modified the coqtop interface by adding an identifier in	ppedrot
2012-05-02	Added an interface call to exit Coqtop nicely.	ppedrot
2012-04-27	Implicit arguments of Definition are taken from the type when given by the user.	pboutill
2012-04-26	migrate g_obligations.ml4 in parsing	letouzey
2012-04-26	Program: avoid staying in program mode after a failed Program command	letouzey
2012-04-23	correct abort in Function when a proof of inversion fails	letouzey
2012-04-19	Supporting optional byte-mark order in utf-8 files (bug #2757).	herbelin
2012-04-18	Corrects a (very) longstanding bug of tactics. As is were, tactic expecting	aspiwack
2012-04-17	Bug 2733 : { } implicits and Fixpoints	pboutill