coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \|	Makefile.install: fix a typo in last commit c954bb5, sorry	Pierre Letouzey	2016-06-24
* \| \| \|	remove an old workaround for OCaml 3.11 + MacOS natdynlink	Pierre Letouzey	2016-06-24
* \| \| \|	Makefile.build: mitigate potential issues with multiple creations of pack .cmi	Pierre Letouzey	2016-06-24
* \| \| \|	Makefile.install: fix the install of plugin cmi	Pierre Letouzey	2016-06-24
* \| \| \|	Better algorithm for variable deambiguation in term printing.	Pierre-Marie Pédrot	2016-06-23
* \| \| \|	Makefile.doc: fix 'make doc'	Pierre Letouzey	2016-06-23
\| * \| \|	Fix typo.	Guillaume Melquiond	2016-06-23
\| * \| \|	Remove extraction-specific code from the checker.	Guillaume Melquiond	2016-06-23
* \| \| \|	Makefile.build: "make;make" should redo nothing	Pierre Letouzey	2016-06-22
* \| \| \|	Makefile: compat5* moved in grammar/, less -I given to camlp4o	Pierre Letouzey	2016-06-21
* \| \| \|	Parsing/compat.ml4: avoid "let open" syntax, unsupported by my camlp5 6.11	Pierre Letouzey	2016-06-21
* \| \| \|	Merge remote-tracking branch 'github/pr/212' into trunk	Maxime Dénès	2016-06-20
\|\ \ \ \
\| \| * \| \|	Reference Manual / Extraction: the original example command no longer works w...	Matej Kosik	2016-06-20
\| * \| \| \|	Add file name, line number and beginning of line position to locations.	Maxime Dénès	2016-06-20
* \| \| \| \|	LtacProf reports structured results (pr/209)	CJ Bell	2016-06-20
* \| \| \| \|	COMMENTS: Vernacexpr.extend_name	Matej Kosik	2016-06-20
* \| \| \| \|	Small optimization in clear_body.	Pierre-Marie Pédrot	2016-06-20
* \| \| \| \|	Fix bug #4825: [clear] should not dependency-check hypotheses that come above...	Pierre-Marie Pédrot	2016-06-20
* \| \| \| \|	Prevent a useless evar normalization in Clenvtac.unify.	Pierre-Marie Pédrot	2016-06-20
* \| \| \| \|	Do not evar-normalize goals when interpreting some hardwired genargs.	Pierre-Marie Pédrot	2016-06-20
\| \| \| * \|	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-19
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge 'pr/215' into trunk	Enrico Tassi	2016-06-19
\|\ \ \ \
* \| \| \| \|	Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot	2016-06-19
\| * \| \| \|	Fix path separator on windows	Jason Gross	2016-06-18
\| * \| \| \|	Fix the build on Windows	Jason Gross	2016-06-18
\|/ / / /
* \| \| \|	Merge PR# 169: Local type-in-type flag.	Pierre-Marie Pédrot	2016-06-18
\|\ \ \ \
\| * \| \| \|	Fixing the checker.	Pierre-Marie Pédrot	2016-06-18
\| * \| \| \|	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
\| * \| \| \|	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
\| * \| \| \|	Print the type-in-type flag in various user-facing functions.	Pierre-Marie Pédrot	2016-06-18
\| * \| \| \|	Adding a local type-in-type flag in kernel declarations.	Pierre-Marie Pédrot	2016-06-18
\|/ / / /
* \| \| \|	Test-suite fix to 1744e37 (injection in context).	Hugo Herbelin	2016-06-18
* \| \| \|	Backporting c064fb933 from 8.5 (another regression with Ltac trace report).	Hugo Herbelin	2016-06-18
* \| \| \|	Adding an "as" clause to specialize.	Hugo Herbelin	2016-06-18
* \| \| \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \| \| \|	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
* \| \| \|	A cleaning phase around delayed induction arg + exporting force_induction_arg.	Hugo Herbelin	2016-06-18
* \| \| \|	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
\| \| * \|	A hack to fix another regression with Ltac trace report in 8.5. E.g.	Hugo Herbelin	2016-06-18
\| * \| \|	Set required version of camlp5 to 6.06.	Maxime Dénès	2016-06-17
\|/ / /
* \| \|	par: like all: but in parallel	Enrico Tassi	2016-06-17
* \| \|	remote counter: avoid thread race on sockets (fix #4823)	Enrico Tassi	2016-06-17
* \| \|	Mentioning goal selectors in CHANGES	Enrico Tassi	2016-06-17
\| * \|	remote counter: avoid thread race on sockets (fix #4823)	Enrico Tassi	2016-06-17
* \| \|	Merge branch 'nzgcd' into trunk	Matthieu Sozeau	2016-06-16
\|\ \ \
\| * \| \|	Remove unneded hints in NZGcd	Matthieu Sozeau	2016-06-16
\|/ / /
* \| \|	proof mode: print unification constraints	Matthieu Sozeau	2016-06-16
* \| \|	Tentative fix of test-suite file to avoid loop	Matthieu Sozeau	2016-06-16
* \| \|	Typeclasses:rename solve_instantiation* & use Hook	Matthieu Sozeau	2016-06-16
* \| \|	Fix resolve_one_typeclass to use the new engine	Matthieu Sozeau	2016-06-16