coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\|\
\| *	Fixing #4644 (regression of unification on evar-evar problems with a match).	Hugo Herbelin	2016-06-09
\| *	Minor simplification in evarconv.ml.	Hugo Herbelin	2016-06-09
\| *	New update on how to find camlp5 binary and library at configure time.	Hugo Herbelin	2016-06-09
\| *	Improve the interpretation scope of arguments of an ltac match.	Hugo Herbelin	2016-06-09
\| *	Reverting dbdff037 which does not seem to prevent to have #3638 fixed	Hugo Herbelin	2016-06-09
* \|	Documenting API changes in dev/doc/changes.txt.	Pierre-Marie Pédrot	2016-06-09
* \|	Merge PR #190: Add configurable shortcuts for user queries to CoqIDE.	Pierre-Marie Pédrot	2016-06-09
\|\ \
* \ \	Merge PR #197.	Pierre-Marie Pédrot	2016-06-09
\|\ \ \
\| \| \| *	Remove failure on non-.v files (bug #4752).	Guillaume Melquiond	2016-06-09
* \| \| \|	Adding profiling developer information in dev/doc/profiling.txt.	Pierre-Marie Pédrot	2016-06-08
\| * \| \|	Add an explicit replacement rule for Refine module	Jason Gross	2016-06-08
\|/ / /
* \| \|	coq_makefile: fix a crucial typo in e9c57a3	Pierre Letouzey	2016-06-08
* \| \|	remove grammar/grammar.mllib	Pierre Letouzey	2016-06-08
* \| \|	Merge branch 'divided-makefile' into trunk	Pierre Letouzey	2016-06-08
\|\ \ \
\| * \| \|	Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}	Pierre Letouzey	2016-06-08
\| * \| \|	Makefile: avoid overwriting test.ml when testing grammar.cma	Pierre Letouzey	2016-06-08
\| * \| \|	Makefile: make clean now removes the .coq-native subdirs	Pierre Letouzey	2016-06-08
\|/ / /
* \| \|	Officially discontinue the experimental coq build via ocamlbuild	Pierre Letouzey	2016-06-08
* \| \|	proofs/proofs.mllib: no more proof_errors !	Pierre Letouzey	2016-06-08
* \| \|	Search interface revisions.	Pierre-Marie Pédrot	2016-06-07
\|\ \ \
\| * \| \|	Removing the convenience functions from the Search API.	Pierre-Marie Pédrot	2016-06-07
\| \| \| *	Fix bug #4777: Printing time is impacted by large terms that don't print.	Pierre-Marie Pédrot	2016-06-07
\| \| \| *	Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).	Guillaume Melquiond	2016-06-07
* \| \| \|	Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunk	Matej Kosik	2016-06-07
\|\ \ \ \
\| * \ \ \	coq_makefile : minor rework	Pierre Letouzey	2016-06-07
\| \|\ \ \ \
\| \| * \| \| \|	Coq_makefile: code cleanup (less long lines, etc)	Pierre Letouzey	2016-06-07
\| \| * \| \| \|	coq_makefile: List.iteri is now standard since OCaml 4.00	Pierre Letouzey	2016-06-07
\| \| * \| \| \|	coq_makefile : short display of commands executed by make	Pierre Letouzey	2016-06-07
\| \| * \| \| \|	coq_makefile: add some -ml-synonym to the ocamldep rules	Pierre Letouzey	2016-06-07
\| \|/ / / /
* \| \| \| \|	typo	Matej Kosik	2016-06-07
* \| \| \| \|	typography	Matej Kosik	2016-06-07
\| * \| \| \|	printing.mllib: remove some other .mli-only from a .mllib	Pierre Letouzey	2016-06-07
\| * \| \| \|	Test for #4787.	Hugo Herbelin	2016-06-07
\| * \| \| \|	Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).	Hugo Herbelin	2016-06-07
\|/ / / /
* \| \| \|	Relying instead on the Coq85 inclusion!	Hugo Herbelin	2016-06-06
* \| \| \|	Mode "Bracketing Last Introduction Pattern" is on for 8.4	Hugo Herbelin	2016-06-06
* \| \| \|	Mode "Regular Subst Tactic" is on in 8.6.	Hugo Herbelin	2016-06-06
* \| \| \|	Merge remote-tracking branch 'github/pr/118' into trunk	Maxime Dénès	2016-06-06
\|\ \ \ \
\| \| \| \| *	Fixing problems introduced in 8.5 with Ltac trace report. E.g.	Hugo Herbelin	2016-06-06
* \| \| \| \|	About printing of traces of failures while calling ltac code.	Hugo Herbelin	2016-06-06
* \| \| \| \|	xmlprotocol: fix unmarshaling of Feedback.Message	Enrico Tassi	2016-06-06
* \| \| \| \|	xmlprotocol: uncomment marshalling code for custom message	Enrico Tassi	2016-06-06
* \| \| \| \|	xmlprotocol: Marshal_error carries the reason	Enrico Tassi	2016-06-06
* \| \| \| \|	Adding the Print Ltac Signatures command.	Pierre-Marie Pédrot	2016-06-05
\|\ \ \ \ \
\| * \| \| \| \|	Adding the Print Ltac Signature command.	Pierre-Marie Pédrot	2016-06-05
\|/ / / / /
* \| \| \| \|	Remove Q_constr from grammar folder.	Pierre-Marie Pédrot	2016-06-05
\|\ \ \ \ \
\| * \| \| \| \|	Removing the Q_constr file.	Pierre-Marie Pédrot	2016-06-05
\| * \| \| \| \|	Moving Hipattern to a regular ML file.	Pierre-Marie Pédrot	2016-06-05
\| * \| \| \| \|	Removing PATTERN uses in Hipattern.	Pierre-Marie Pédrot	2016-06-05
\|/ / / / /