coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|/\|
\| *	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
* \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
* \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-13
\|\
\| *	Fixing printing of evar name in an error message of instantiate.	Hugo Herbelin	2016-07-13
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Extruding the code for the Existential command from Proofview.	Pierre-Marie Pédrot	2016-03-20
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Update headers.	Maxime Dénès	2015-01-12
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Better structure for Ltac pretyping environments.	Pierre-Marie Pédrot	2014-08-07
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Monomorphization (proof)	ppedrot	2012-11-25
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	Revise API of understand_ltac to be parameterized by a flag for resolution of...	msozeau	2012-03-14
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin	2009-12-24
*	Take constraints into account in the "instantiate" tactic	herbelin	2009-10-30
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin	2009-04-24