coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Updated debugging printers	Hugo Herbelin	2014-04-01
*	app_node, stack, state printers	Pierre Boutillier	2014-02-24
*	'Pretty' printer for wf_paths	Pierre	2014-01-11
*	Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd	Pierre Letouzey	2014-01-08
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Removes Refine from the dev tools now that the module has been deleted.	aspiwack	2013-11-02
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	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