coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl	letouzey	2012-03-30
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey	2012-03-23
*	Remove undocumented command "Delete foo"	letouzey	2012-03-23
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin	2012-03-20
*	Force Check (which, from 8.4beta, accepts unresolved evars) to however	herbelin	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Fix merge and add missing file.	msozeau	2012-03-14
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Integrated obligations/eterm and program well-founded fixpoint building to to...	msozeau	2012-03-14
*	Everything compiles again.	msozeau	2012-03-14
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02