coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6736: [toplevel] Move beautify to its own pass.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6882: Harden gitattributes against core.whitespace configuration.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6676: [proofview] goals come with a state	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #915: Fix rewrite in * side conditions	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Removing test for bug #2850.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Adding a test file for evar handling in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[compat] Remove "Tactic Pattern Unification"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[compat] Remove "Intuition Iff Unfolding"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[compat] Remove "Injection L2R Pattern Order"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	CHANGES entry for #6791.	Théo Zimmermann	2018-03-02
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Remove VOld compatibility flag.	Théo Zimmermann	2018-03-02
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Turn warning for deprecated notations on.	Théo Zimmermann	2018-03-02
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Remove the deprecation for some 8.2-8.5 compatibility aliases.	Théo Zimmermann	2018-03-02
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[VM] Unify Const_sorts and Const_type, and remove Vsort.	Maxime Dénès	2018-03-02
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \|	[stm] Partial fix for bug #6884 [location missing from replay nodes]	Emilio Jesus Gallego Arias	2018-03-02
\| \| \| \| \| * \| \| \| \| \| \| \| \|	Harden gitattributes against core.whitespace configuration.	Gaëtan Gilbert	2018-03-01
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \|	Fix #6878: univ undefined for [with Definition] bad instance size.	Gaëtan Gilbert	2018-03-01
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \|	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
\| \| \| \|_\|/ / / / / / / \| \| \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \|	Moving code for "simple induction"/"simple destruct" to coretactics.ml4.	Hugo Herbelin	2018-03-01
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6856: travis: elpi needs findlib >= 1.5	Maxime Dénès	2018-03-01
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6864: Remove empty, wrongly located, doc file.	Maxime Dénès	2018-03-01
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6861: Typo in the documentation of the `pattern` tactic	Maxime Dénès	2018-03-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6850: Fix #6751 trust_file_cache logic was inverted	Maxime Dénès	2018-03-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[toplevel] Update state when `Drop` exception is thrown [#6872]	Emilio Jesus Gallego Arias	2018-02-28
\| \| \| \| \| \| \| \|/ / / / / / / \| \| \| \| \| \| \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \|	[toplevel] Move beautify to its own pass.	Emilio Jesus Gallego Arias	2018-02-28
\| \| \| \| \| \| \|_\|_\|_\|/ / / / \| \| \| \| \| \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \|	[test-suite] Add a basic test-case for `Load`.	Emilio Jesus Gallego Arias	2018-02-28
\| \| \| \| \| * \| \| \| \| \| \| \|	[toplevel] [vernac] Remove Load hack and check supported scenarios.	Emilio Jesus Gallego Arias	2018-02-28
\| \| \| \| \| \|/ / / / / / /
\| \| \| \| \| \| \| \| * / / /	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\| \| \| \| \| \| \|_\|/ / / / \| \| \| \| \| \|/\| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	travis: elpi needs findlib >= 1.5	Enrico Tassi	2018-02-28
\| \| \| \| * \| \| \| \| \| \|	tavis: make the . in pkg.version part of $VERSION	Enrico Tassi	2018-02-28
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6847: Fix make source-doc	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6854: comment "resolvability" bit in Evd.evar_map	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6852: [stdlib] move “Require” out of sections	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6756: Fix issue with spurious timing test failures	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6789: Check whitespace errors per-commit.	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...	Maxime Dénès	2018-02-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \