coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	Some documentation of recent changes concerning interfaces	letouzey	2012-05-29
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29
*	Extend become a mli-only file in intf/	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
*	Strongly reduce the dependencies of grammar.cma, modulo two hacks	letouzey	2012-05-29
*	Pattern as a mli-only file, operations in Patternops	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Vernacexpr is now a mli-only file, locality stuff now in locality.ml	letouzey	2012-05-29
*	Coqide MacOS integration refresh	pboutill	2012-04-27
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Removing Dhyp from debugger.	herbelin	2012-04-06
*	Everything compiles again.	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin	2012-02-01
*	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin	2012-01-20
*	Suspending declaration of undefined debug printers.	herbelin	2011-12-18
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Revert "New evar_map printer ppevmfull which can typically be installed for"	herbelin	2011-10-17
*	New evar_map printer ppevmfull which can typically be installed for	herbelin	2011-10-17
*	dev/base_include: display a nice message at the end of the load	letouzey	2011-10-15
*	debugging.txt: no more typing of #use "include" if using .ocamlinit	letouzey	2011-10-15
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin	2011-10-01
*	Polishing commits r14492, r14448 and r14407 (tactics propagate	herbelin	2011-09-25
*	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau	2011-08-04
*	Add printer dependency to Hashtbl_alt (used in Term)	puech	2011-07-29
*	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin	2011-07-18
*	Finally, pr_goal seems to work for printing v8.2 style goal in debugger.	herbelin	2011-07-16
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	A few comments and a dev file to summarize issues with unification	herbelin	2011-06-13
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	As many notation for for vectors as for List.	pboutill	2011-05-03
*	dev/base_include: no more mod_self_id	letouzey	2011-04-26
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Fix dev/base_include after change of constant_body	letouzey	2011-04-06
*	Adapt printers.mllib after my last commit	letouzey	2011-03-16
*	Annotations at functor applications:	letouzey	2011-02-11
*	Update changelogs	glondu	2011-02-11
*	Factorize code of rewrite to make way for a new implementation using the	msozeau	2011-02-07
*	Remove obsolete script univdot, update dev doc about universes	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Prepare change of nomenclature rawconstr -> glob_constr	glondu	2010-12-23