coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing #5460 (limitation in computing deps in pattern-matching compilation).	Hugo Herbelin	2017-04-08
*	Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).	Hugo Herbelin	2017-01-22
*	Document changes	Matthieu Sozeau	2016-12-02
*	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
*	Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).	Hugo Herbelin	2016-10-29
*	Attempt to improve error rendering in pattern-matching compilation (#5142).	Hugo Herbelin	2016-10-19
*	Completing reverting generalization and cleaning of the return clause inference.	Hugo Herbelin	2016-10-13
*	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
*	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
*	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin	2016-09-26
*	Trying an abstracting dependencies heuristic for the match return clause even...	Hugo Herbelin	2016-09-26
*	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin	2016-09-26
*	Inference of return clause: giving uniformly priority to "small inversion".	Hugo Herbelin	2016-09-26
*	Fixing a bug in the presence of let-in while inferring the return clause.	Hugo Herbelin	2016-08-20
*	Disallow dependent case on prim records w/o eta	Matthieu Sozeau	2016-07-06
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Program: cleanup in cases, add options	Matthieu Sozeau	2016-06-29
*	Rework treatment of default transparency of obligations	Matthieu Sozeau	2016-06-27
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\
* \|	Revert "Add support for generalization also on named variables in pattern-mat...	Hugo Herbelin	2016-04-27
* \|	Revert "Add support for deep dependencies in variables within the recursive s...	Hugo Herbelin	2016-04-27
* \|	Revert "Fixing a De Bruijn bug in computing return predicate by inversion."	Hugo Herbelin	2016-04-27
* \|	Revert "Using existing names as a basis for the inner names of the pattern-ma...	Hugo Herbelin	2016-04-27
* \|	Revert "Vers un filtrage profond ..."	Hugo Herbelin	2016-04-27
* \|	Vers un filtrage profond ...	Hugo Herbelin	2016-04-27
* \|	Using existing names as a basis for the inner names of the pattern-matching p...	Hugo Herbelin	2016-04-27
* \|	Fixing a De Bruijn bug in computing return predicate by inversion.	Hugo Herbelin	2016-04-27
* \|	Add support for deep dependencies in variables within the recursive structure.	Hugo Herbelin	2016-04-27
* \|	Add support for generalization also on named variables in pattern-matching	Hugo Herbelin	2016-04-27
\| *	Optimization in building a return clause by pattern-matching: do not	Hugo Herbelin	2016-04-27
* \|	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	About building of substitutions from instances.	Hugo Herbelin	2015-12-05
\|/
*	Using appropriate lambda decomposition function counting let-ins when	Hugo Herbelin	2015-10-18
*	Fix inference of return clause raising a type error.	Matthieu Sozeau	2015-10-09
*	Univs: fix bug #4161.	Matthieu Sozeau	2015-10-08
*	Documenting the code when preference is given to expansion of default	Hugo Herbelin	2015-09-08
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Fixing first part of bug #3210 (inference of pattern-matching return	Hugo Herbelin	2015-02-27
*	Fixing #4001 (missing type constraints when building return clause of match).	Hugo Herbelin	2015-02-10
*	Update headers.	Maxime Dénès	2015-01-12
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	Fixing wrong evar_map in return clause inference, revealed by 48509b611.	Hugo Herbelin	2014-12-08
*	Improved tracking of the origin of evars.	Hugo Herbelin	2014-12-07