coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2017-01-23
*	Document changes	Matthieu Sozeau	2016-12-02
*	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
*	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\|\
\| *	Fixes to compile with ocaml 4.01	Matthieu Sozeau	2016-11-07
* \|	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\|\ \ \| \|/ \|/\|
* \|	Merge remote-tracking branch 'github/pr/321' into v8.6	Maxime Dénès	2016-10-28
\|\ \
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\| \| *	Unification constraint handling (#4763, #5149)	Matthieu Sozeau	2016-10-22
\| \|/ \|/\|
* \|	Oops, my bad, didn't expect a merge issue!	Matthieu Sozeau	2016-10-21
* \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
\| *	sections/hints: prevent Not_found in get_type_of	Matthieu Sozeau	2016-10-21
\|/
*	Fix bug #5145: Anomaly: index to an anonymous variable.	Pierre-Marie Pédrot	2016-10-15
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
*	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\|\
* \|	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
\| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\|/
*	Fast path in push_rel_context_to_named_context.	Pierre-Marie Pédrot	2016-09-05
*	Fast path in whd_evar.	Pierre-Marie Pédrot	2016-09-02
*	Short documentation, filling TODO's in evd.mli.	Hugo Herbelin	2016-09-01
*	Do not export an internal function in Namegen.	Pierre-Marie Pédrot	2016-08-25
*	Two protections against failures when printing evar_map.	Hugo Herbelin	2016-08-17
*	Fixing printing in debugger (no global env in debugger).	Hugo Herbelin	2016-08-17
*	Efficiently generate the pretyping contexts.	Pierre-Marie Pédrot	2016-08-16
\|\
* \|	Remove unused optional "predicative" argument.	Guillaume Melquiond	2016-08-10
\| *	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot	2016-08-06
\| *	Using the extended contexts in pretyping.	Pierre-Marie Pédrot	2016-08-05
\| *	Use sets instead of lists for names to avoid in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| *	Simplifying code in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| *	Exporting the renaming API for evar declaration.	Pierre-Marie Pédrot	2016-08-04
\|/
*	Fixing #4906 (regression in printing an error message).	Hugo Herbelin	2016-07-08
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Univ: Use loc even if there are more unbound levels	Matthieu Sozeau	2016-06-29
*	Univs: add source locations of levels	Matthieu Sozeau	2016-06-29
*	Optmimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
*	Better algorithm for variable deambiguation in term printing.	Pierre-Marie Pédrot	2016-06-23
*	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
*	Proofview: extensions for backtracking eauto	Matthieu Sozeau	2016-06-16
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
* \	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \
\| \| *	Fix a typo in proofs/proofview.mli.	Cyprien Mangin	2016-06-14
\| \| *	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
\| \| *	Add a comment about the use of a zipper, for clarity.	Cyprien Mangin	2016-06-14
\| \| *	Add a [CList.partitioni] function.	Cyprien Mangin	2016-06-14
\| \| *	Add goal range selectors.	Cyprien Mangin	2016-06-14
\| \|/ \|/\|
* \|	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09