coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix a bug in cumulativity	Amin Timany	2017-06-16
*	A short cleanup	Amin Timany	2017-06-16
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	fix dev/base_include (thanks Zimmi48)	Pierre Letouzey	2017-06-15
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)	Matthieu Sozeau	2017-04-07
*	Fixing #use"include" after vernac is added and ltac is moved to a plugin.	Hugo Herbelin	2017-02-23
*	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
*	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\
\| *	Fixing another instance of bug #3267 in eauto, this time in the	Hugo Herbelin	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Fixing #4198 (looking for subterms also in the return clause of match).	Hugo Herbelin	2015-04-21
* \|	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot	2015-02-27
\|/
*	Removing import of Proofview in debugger because its module Goal hides	Hugo Herbelin	2014-12-07
*	More "open" by default for trace debugging.	Hugo Herbelin	2014-10-31
*	Fix ill-typed debugging function	Matthieu Sozeau	2014-10-15
*	Add debug printers for projections, fix printing of evar constraints	Matthieu Sozeau	2014-10-10
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	Fix base_include due to change in argument order of env and evar_map	Matthieu Sozeau	2014-09-12
*	More open in base_include	Hugo Herbelin	2014-06-28
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	Remove Lemmas from base_include, it's not linked in dev/printers anymore	Matthieu Sozeau	2014-05-06
*	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