coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Use msg_info for LtacProf	Jason Gross	2017-12-11
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Allow LtacProf tactics to be called	Jason Gross	2017-12-11
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6312: [configure] fix detection of `md5sum`	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Catch errors while coercing 'and' intro patterns	Tej Chajed	2017-12-11
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Fix issue #6387	Martin Vassor	2017-12-11
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6331: Linter: skip PRs older than the linter.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6311: Don't Add LoadPath on CoqIDE startup, #6153	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Fix anomaly in [Type foo] command, + print uctx like Check.	Gaëtan Gilbert	2017-12-11
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Restoring filtering of native files passed to `rm` during `make clean`.	Maxime Dénès	2017-12-11
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Add overlay.	Théo Zimmermann	2017-12-11
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Remove deprecated appcontext and corresponding documentation.	Théo Zimmermann	2017-12-11
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Remove deprecated option Dependent Propositions Eliminiation.	Théo Zimmermann	2017-12-11
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[flags] [stm] Reorganize flags.	Emilio Jesus Gallego Arias	2017-12-11
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[stm] Move process_id to Spawned.	Emilio Jesus Gallego Arias	2017-12-11
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6352: [makefile] Address #6291: install more development files.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1150: [stm] Remove all but one use of VtUnknown.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6338: Remove up-to-conversion term matching	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6363: [META] Some dependency fixes.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6351: Fix a copy-paste error in ci-ltac2.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6346: [ci] CoLoR has moved to github	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6340: [default.nix] Add ocpIndent and ocp-index.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Axiom-free proof of eta expansion.	Jasper Hugunin	2017-12-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[make] remove unneeded generated file "tolink.ml"	Emilio Jesus Gallego Arias	2017-12-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias	2017-12-10
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6370: [ci] Temporal workaround for checker non-backwards compatible...	Maxime Dénès	2017-12-10
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci] Temporal workaround for checker non-backwards compatible change.	Emilio Jesus Gallego Arias	2017-12-10
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| \| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[META] Some dependency fixes.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|_\|_\|_\|/ / / / / / / / / / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[stm] Remove all but one use of VtUnknown.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[summary] Adapt STM to the new Summary API.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[summary] Allow typed projections from global state + rework of internals.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[lib] Convenience function for `Dyn.Easy`	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove up-to-conversion matching functions.	Pierre-Marie Pédrot	2017-12-09
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Remove most uses of function extensionality in Program.Combinators	Jasper Hugunin	2017-12-09
\| \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci] Download ci-sf archives into the proper CI build dir.	Emilio Jesus Gallego Arias	2017-12-09
\| \|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Revert "CI: poc Circleci configuration"	Arnaud Spiwack	2017-12-08
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	CI: poc Circleci configuration	Arnaud Spiwack	2017-12-08
\|/ / / / / / / / / / / / / / / / /
\| \| \| \| \| \| * / / / / / / / / / /	[makefile] Address #6291: install more development files.	Emilio Jesus Gallego Arias	2017-12-08
\| \|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Fix a copy-paste error in ci-ltac2.	Théo Zimmermann	2017-12-08
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6334: Remove dead code in Reductionops	Maxime Dénès	2017-12-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \