coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\
\| *	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
* \|	Move is_prim... to Inductiveops and correct Scheme	Matthieu Sozeau	2016-07-06
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
\| *	A hack to fix another regression with Ltac trace report in 8.5. E.g.	Hugo Herbelin	2016-06-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\\|
\| *	Reserve exception "ConversionFailed" in unification for failure of	Hugo Herbelin	2016-06-12
\| *	Fixing bug in printing CannotSolveConstraint (collision of context names).	Hugo Herbelin	2016-06-12
\| *	Fixing problems introduced in 8.5 with Ltac trace report. E.g.	Hugo Herbelin	2016-06-06
* \|	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot	2016-03-20
* \|	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20
* \|	Removing dependency of Himsg in tactic files.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving Ltac traces to Tacexpr and Tacinterp.	Pierre-Marie Pédrot	2016-03-06
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \| \| \|/ \| \|/\|
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
\| *	Improving error message with missing patterns in the presence of	Hugo Herbelin	2016-02-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fixing bug #3826: "Incompatible module types" is uninformative.	Pierre-Marie Pédrot	2016-01-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove useless rec flags.	Guillaume Melquiond	2016-01-02
* \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\|
* \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\| *	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
\|/
*	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey	2015-10-25
*	Fixing bug #4367: Wrong error message in unification.	Pierre-Marie Pédrot	2015-10-14
*	Also there's an extra space in the error message.	mlasson	2015-09-03
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Better error message for nested module application.	Maxime Dénès	2015-02-13
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Avoiding a redundant information in unification error message.	Hugo Herbelin	2015-01-11
*	Added a CannotSolveConstraint unification error and made experiments	Hugo Herbelin	2014-12-11
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	Improved tracking of the origin of evars.	Hugo Herbelin	2014-12-07
*	Improving error message when one instance-hole is not found.	Hugo Herbelin	2014-12-04
*	Slight improving of a unification error message.	Hugo Herbelin	2014-12-03
*	Removing superfluous newlines in setoid_rewrite error message.	Hugo Herbelin	2014-11-22
*	Fixing a little bug with nested but convertible occurrences in "destruct at".	Hugo Herbelin	2014-11-18
*	Continuing 3741c46fe134 on reporting ltac error.	Hugo Herbelin	2014-11-08
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Add debug printers for projections, fix printing of evar constraints	Matthieu Sozeau	2014-10-10
*	Fixing #3634 (wrong env in "cannot instantiate because not in its	Hugo Herbelin	2014-10-03
*	Implement module subtyping for polymorphic constants (errors on	Matthieu Sozeau	2014-10-02
*	Print type and environment of unsolved holes.	Arnaud Spiwack	2014-10-02
*	Fixing nice printing of error reporting with ml tactics bound to ltac names.	Hugo Herbelin	2014-10-01
*	Fixing bug #3646.	Pierre-Marie Pédrot	2014-09-19
*	Be more conservative and keep the use of eq_constr in pretyping/ functions.	Matthieu Sozeau	2014-09-17
*	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau	2014-09-17