coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	FIX: a bug in the pattern matching	Matej Kosik	2016-09-28
*	8.7 now points to Current and 8.6 points to V8_6.	Théo Zimmermann	2016-09-28
*	Add a compatibility flag for 8.6 and refactor.	Théo Zimmermann	2016-09-28
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-27
\| \|\
\| * \|	LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)	Enrico Tassi	2016-09-27
\| * \|	Remove spaces from around list notations	Jason Gross	2016-09-26
\| * \|	Remove spaces from around vector notations	Jason Gross	2016-09-26
\| * \|	Unbreak Ltac [ \| .. \| ] notation in -compat 8.5	Jason Gross	2016-09-26
\| * \|	Fix bug #4785 (use [ ] for vector nil)	Jason Gross	2016-09-26
\| * \|	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
\| * \|	Fast russian peasant exponentiation in Nsatz.	Pierre-Marie Pédrot	2016-09-26
\| * \|	Monomorphizing various uses of arrays in Nsatz.	Pierre-Marie Pédrot	2016-09-26
\| * \|	Partial fix for bug #5085: nsatz_compute stack overflows.	Pierre-Marie Pédrot	2016-09-26
\| * \|	Fix bug #5093: typeclasses eauto depth arg does not accept a var.	Pierre-Marie Pédrot	2016-09-26
\| * \|	Fix bug #5090: Effect of -Q depends on coqtop's current directory.	Pierre-Marie Pédrot	2016-09-25
\| * \|	The coqtop options -Q and -R do not affect the ML loadpath anymore.	Pierre-Marie Pédrot	2016-09-25
\| * \|	Moving "move" in the new proof engine.	Hugo Herbelin	2016-09-24
\| \| *	Ensuring that the evar name is preserved by "rename" as it is already	Hugo Herbelin	2016-09-24
\| * \|	Adding a test for bug #5096.	Pierre-Marie Pédrot	2016-09-24
\| * \|	Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].	Pierre-Marie Pédrot	2016-09-23
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-23
\| \|\\|
\| * \|	coqc -o now places .glob file near .vo file	Enrico Tassi	2016-09-22
\| * \|	typos	Enrico Tassi	2016-09-22
* \| \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \| \|	Merge remote-tracking branch 'github/pr/283' into trunk	Maxime Dénès	2016-09-22
\|\ \ \
\| \| \| *	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
* \| \| \|	Removing dead code in CoqIDE.	Pierre-Marie Pédrot	2016-09-21
* \| \| \|	Fix an error-prone error API.	Pierre-Marie Pédrot	2016-09-21
* \| \| \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
\| \| * \|	Fix description of change in intro semantics.	Maxime Dénès	2016-09-21
\| * \| \|	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
\| * \| \|	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
\|/ / /
\| * \|	Remove dead code in library/lib.ml.	Maxime Dénès	2016-09-20
\| \| *	Replace { command ; } with ( command )	Erik Martin-Dorel	2016-09-19
\| \| *	Fix typos in RefMan-uti.tex.	Erik Martin-Dorel	2016-09-19
* \| \|	Fixing test FunExt.v.	Hugo Herbelin	2016-09-19
\| * \|	Fix warning when using Variables at toplevel.	Maxime Dénès	2016-09-19
* \| \|	extensionality: Handle dependently-used hypotheses	Jason Gross	2016-09-19
* \| \|	Adding an "extensionality in H" tactic which applies functional	Hugo Herbelin	2016-09-19
\| * \|	Further "decide equality" tests on demand of Jason.	Hugo Herbelin	2016-09-17
\| * \|	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
\| * \|	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
* \| \|	Make the Coq codebase independent from Ltac-related code.	Pierre-Marie Pédrot	2016-09-16
\|\ \ \
\| * \| \|	Documenting API changes.	Pierre-Marie Pédrot	2016-09-15
\| * \| \|	Moving Tacexpr to ltac/ folder.	Pierre-Marie Pédrot	2016-09-15