coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update debug code according to reorganization into modules.	msozeau	2013-02-27
*	Adapt dev/base_include to new Declarations	letouzey	2013-02-27
*	Added Evarsolve to the list of modules to open for debugging.	herbelin	2013-02-21
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	place all pretty-printing files in new dir printing/	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
*	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
*	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin	2012-02-01
*	dev/base_include: display a nice message at the end of the load	letouzey	2011-10-15
*	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
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Quick fix for having clenv debug printer working in trunk.	herbelin	2010-06-18
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Fixed "Scheme Equality" when another instance of the scheme on the	herbelin	2009-11-08
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin	2009-08-07
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19
*	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin	2008-09-02
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	- Add pretty-printers for Idpred, Cpred and transparent_state, used for	msozeau	2008-04-24
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Ocaml toplevel convenience.	glondu	2007-12-07
*	- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)	herbelin	2007-08-22
*	Export de l'afficheur de substitutions de noms de modules pour le débogueur	herbelin	2007-01-19
*	PÃrÃ©ouverture de la plupart des fichis pour Ã©viter d'avoir Ã qualifier	herbelin	2006-05-23
*	Ajout printer Idset.t	herbelin	2006-01-29
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)	herbelin	2006-01-04
*	MAJ restructuration constrintern.ml	herbelin	2005-12-23
*	Ajout constant printer	herbelin	2005-02-18
*	Découpage des printers pour ne pas avoir de dépendances en la vm dans les p...	herbelin	2005-01-02
*	Ajout printer bigint	herbelin	2004-12-29
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Ajout translate	herbelin	2003-04-07
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	Parsing	herbelin	2001-08-10
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Modification pour passage p-automates	mohring	2001-05-15