coq - The formal proof system

Age	Commit message (Expand)	Author
2017-12-14	Document Record Elimination Schemes.	Gaëtan Gilbert
2017-12-14	Document Asymmetric Patterns.	Gaëtan Gilbert
2017-12-14	Document some omega options (missing Omega Oldstyle).	Gaëtan Gilbert
2017-12-14	Circle CI: add badge to README.	Gaëtan Gilbert
2017-12-14	Add doc for Set Debug RAKAM.	Gaëtan Gilbert
2017-12-14	Add doc for Set Debug Cbv.	Gaëtan Gilbert
2017-12-14	Add doc for Set Info/Debug Auto/Trivial/Eauto.	Gaëtan Gilbert
2017-12-14	Add optindex for Set Bullet Behavior.	Gaëtan Gilbert
2017-12-14	Add doc for Set Congruence Verbose	Gaëtan Gilbert
2017-12-14	Circle CI: separate job to boot opam with all used packages.	Gaëtan Gilbert
2017-12-14	Circle CI: remove warning jobs	Gaëtan Gilbert
2017-12-14	Circle CI: cat failed test suite logs	Gaëtan Gilbert
2017-12-14	Fix typo in doc optindex for Typeclass Resolution ...	Gaëtan Gilbert
2017-12-14	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès
2017-12-14	Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards com...	Maxime Dénès
2017-12-14	Merge PR #6388: Fix issue #6387	Maxime Dénès
2017-12-13	Merge PR #1108: [stm] Reorganize flags	Maxime Dénès
2017-12-13	Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.	Maxime Dénès
2017-12-13	Merge PR #6251: [proof] Embed evar_map in RefinerError exception.	Maxime Dénès
2017-12-13	Merge PR #6175: Restoring filtering of native files passed to `rm` during `ma...	Maxime Dénès
2017-12-13	[meta] Minor linking fix.	Emilio Jesus Gallego Arias
2017-12-13	[econstr] Small cleanup in `vernac/lemmas`	Emilio Jesus Gallego Arias
2017-12-13	[econstr] Add a couple of new API functions.	Emilio Jesus Gallego Arias
2017-12-13	[lib] Auxiliary functions in List + fixes.	Emilio Jesus Gallego Arias
2017-12-13	Circle CI: uses dependencies between external developments.	Gaëtan Gilbert
2017-12-13	Put bignums, math-classes and corn dependencies in Makefile	Gaëtan Gilbert
2017-12-13	Circle CI: enable TIMED for external developments	Gaëtan Gilbert
2017-12-13	Circle CI: use cache for opam	Gaëtan Gilbert
2017-12-13	Circle CI: enable native compiler.	Gaëtan Gilbert
2017-12-12	Fix #5081 by more fine-grained LtacProf recording	Jason Gross
2017-12-13	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias
2017-12-12	Near-full implementation of Circle CI.	Gaëtan Gilbert
2017-12-12	Documenting the new options for printing "match".	Hugo Herbelin
2017-12-12	Decompiling pattern-matching: mini-removal dead code.	Hugo Herbelin
2017-12-12	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin
2017-12-12	Removing cumbersome location in multiple patterns.	Hugo Herbelin
2017-12-12	Improving spacing in printing disjunctive patterns.	Hugo Herbelin
2017-12-12	Revert "[ci] Temporal workaround for checker non-backwards compatible change."	Théo Zimmermann
2017-12-12	Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts	Maxime Dénès
2017-12-12	Further clean-up in Reductionops, removing unused lift arguments.	Maxime Dénès
2017-12-12	Merge PR #6359: Remove most uses of function extensionality in Program.Combin...	Maxime Dénès
2017-12-12	Merge PR #6275: [summary] Allow typed projections from global state.	Maxime Dénès
2017-12-11	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	CI: poc Circleci configuration	Arnaud Spiwack
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