coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Cleanup debug printers a bit, add generated mli.	Gaëtan Gilbert	2017-12-22
*	Adding econstr printer to "include" file.	Hugo Herbelin	2017-07-12
*	Fix a bug in cumulativity	Amin Timany	2017-06-16
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Adding a printer for Proof.proof reflecting the focusing layout.	Hugo Herbelin	2017-01-26
*	FIX: dev/include	Matej Kosik	2016-11-05
*	A fix to dev/include.	Hugo Herbelin	2016-08-17
*	More printers in tracer.	Hugo Herbelin	2014-12-05
*	Adding printers for ppproofview.	Hugo Herbelin	2014-10-13
*	Adding printer for named_context_val and Goal.goal in debugger.	Hugo Herbelin	2014-10-09
*	Adding a printer for hints.	Hugo Herbelin	2014-10-07
*	Debug RAKAM	Pierre Boutillier	2014-08-26
*	- Fix bug #3368, due to wrong use of the Cst_stack for projections.	Matthieu Sozeau	2014-06-11
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Fix issue #88: restrict_universe_context was wrongly forgetting about constra...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	print futures in caml toplevel too	Enrico Tassi	2014-04-25
*	Set officially the minimal OCaml requirement to 3.12.1	Pierre Letouzey	2014-03-02
*	- install evar printer for debugging	msozeau	2013-10-29
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	remove a warning after Drop about print_hint_db	letouzey	2013-02-27
*	Revert "Fixing include printers"	pboutill	2012-08-05
*	Fixing include printers	ppedrot	2012-08-03
*	Suspending declaration of undefined debug printers.	herbelin	2011-12-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	debugging.txt: no more typing of #use "include" if using .ocamlinit	letouzey	2011-10-15
*	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau	2011-08-04
*	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin	2011-07-18
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Factorize code of rewrite to make way for a new implementation using the	msozeau	2011-02-07
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Remove useless ppevd (which is identical to ppevm)	glondu	2009-11-13
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin	2009-05-20
*	Execute #rectypes directive in embedded OCaml toplevel...	glondu	2008-11-19
*	Hint for Debian users.	glondu	2008-03-18
*	Add printer for Pp.std_ppcmds...	msozeau	2008-02-08
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Ocaml toplevel convenience.	glondu	2007-12-07
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin	2005-12-26
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	unification encore...	barras	2004-09-08
*	prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech...	letouzey	2003-04-16
*	Ajout affichage fconstr	herbelin	2002-12-05
*	ajout d'un printer pour les global_reference	letouzey	2002-11-04