coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.	Matthieu Sozeau	2018-07-09
\|\
* \|	Add test for #8004.	Gaëtan Gilbert	2018-07-06
* \|	Convert timing tools to run with both python2 and python3	Jasper Hugunin	2018-07-04
* \|	Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands	Pierre-Marie Pédrot	2018-07-03
\|\ \
\| * \|	hints: add Hint Variables/Constants Opaque/Transparent commands	Matthieu Sozeau	2018-07-02
* \| \|	Add test for Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\|/ /
* \|	Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...	Emilio Jesus Gallego Arias	2018-07-01
\|\ \
* \| \|	Workaround to fix #7731 (printing not splitting line at break hint).	Hugo Herbelin	2018-06-29
\| * \|	Fixes #7712 (an anomaly in reporting bad recursive notation format).	Hugo Herbelin	2018-06-29
\|/ /
* \|	Merge PR #7860: Fix #7704: Launching coqide through PATH fails.	Emilio Jesus Gallego Arias	2018-06-28
\|\ \
* \ \	Merge PR #7866: Implementation of mutual records in the higher strata	Maxime Dénès	2018-06-28
\|\ \ \
* \ \ \	Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \
\| * \| \| \|	Test file for #7723	Maxime Dénès	2018-06-27
* \| \| \| \|	Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).	Hugo Herbelin	2018-06-26
\|/ / / /
* \| \| \|	Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...	Matthieu Sozeau	2018-06-25
\|\ \ \ \
* \ \ \ \	Merge PR #7559: Existing Class noop when already a class + warning.	Matthieu Sozeau	2018-06-25
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7620: [ssr] rewrite: turn anomaly into regular error	Maxime Dénès	2018-06-25
\|\ \ \ \ \ \
\| \| \| \| * \| \|	Adding various tests for mutual records.	Pierre-Marie Pédrot	2018-06-24
\| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7236: [ssr] simpler semantics for delayed clears	Maxime Dénès	2018-06-23
\|\ \ \ \ \ \
\| \| \| \| \| * \|	Fix #7704: get_toplevel_path needs normalised argv.(0)	Gaëtan Gilbert	2018-06-22
\| \| \| \| * \| \|	Remove hack skipping comparison of algebraic universes in subtyping.	Gaëtan Gilbert	2018-06-22
\| * \| \| \| \| \|	[ssr] implement {}/v as a short hand for {v}/v when v is an id	Enrico Tassi	2018-06-22
\| \| \|_\|/ / / \| \|/\| \| \| \|
* / \| \| \| \|	[ssr] test case for rewrite and set on univ poly keys	Enrico Tassi	2018-06-22
\|/ / / / /
\| \| \| \| *	Fix #5719: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot	2018-06-21
\| \|_\|_\|/ \|/\| \| \|
\| * \| \|	[ssr] test case for rewrite (setoid) making the goal illtyped	Enrico Tassi	2018-06-20
\|/ / /
* \| \|	Merge PR #6754: Better elaboration of pattern-matchings on primitive projections	Pierre-Marie Pédrot	2018-06-19
\|\ \ \
* \| \| \|	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related t...	Pierre-Marie Pédrot	2018-06-17
\|\ \ \
* \ \ \	Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretyping	Pierre-Marie Pédrot	2018-06-17
\|\ \ \ \
\| \| * \| \|	Fixes #7811 (uncaught Not_found in notation printer related to "match").	Hugo Herbelin	2018-06-17
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.	Maxime Dénès	2018-06-17
\|\ \ \ \
\| \| \| * \|	Add test-suite case for performance, had to use Timeout	Matthieu Sozeau	2018-06-15
\| \| \| * \|	Better elaboration of pattern-matchings on primitive projections	Matthieu Sozeau	2018-06-15
\| \|_\|/ / \|/\| \| \|
\| \| * \|	Do not allow spliting in res_pf, this is reserved for pretyping	Matthieu Sozeau	2018-06-15
* \| \| \|	Workaround to handle non-value arguments in tactics.	Cyprien Mangin	2018-06-14
\| \|/ / \|/\| \|
* \| \|	Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...	Pierre-Marie Pédrot	2018-06-14
\|\ \ \
* \ \ \	Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...	Matthieu Sozeau	2018-06-14
\|\ \ \ \
* \ \ \ \	Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...	Matthieu Sozeau	2018-06-14
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7771: Tweak printing boxes for unicode binders	Hugo Herbelin	2018-06-14
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Markdown docs: switch from absolute to relative links.	Théo Zimmermann	2018-06-13
* \| \| \| \| \| \|	Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").	Hugo Herbelin	2018-06-12
\| \| * \| \| \| \|	Fixes #7780 (missing lift in expanding alias under a binder in unification).	Hugo Herbelin	2018-06-12
\| \|/ / / / / \|/\| \| \| \| \|
\| * \| \| \| \|	Tweak printing boxes for unicode binders	Ralf Jung	2018-06-10
* \| \| \| \| \|	Fixing #7700 (section variables bound to abbreviations were not found).	Hugo Herbelin	2018-06-10
\|/ / / / /
\| \| \| \| *	Existing Class noop when already a class + warning.	Gaëtan Gilbert	2018-06-08
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	add test for #7595	Ralf Jung	2018-06-07
\| \| \| *	Fix #7615: Functor inlining drops universe substitution.	Pierre-Marie Pédrot	2018-06-07
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...	Maxime Dénès	2018-06-05
\|\ \ \
* \ \ \	Merge PR #7663: test suite: make target to regenerate failing output tests	Enrico Tassi	2018-06-05
\|\ \ \ \
* \| \| \| \|	Fix #7631: native_compute fails to compile an example in Coq 8.8	Maxime Dénès	2018-06-04