aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-22Reorder dev/dbGaëtan Gilbert
2017-12-22Cleanup top_printers.mliGaëtan Gilbert
2017-12-22Cleanup debug printers a bit, add generated mli.Gaëtan Gilbert
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-15Merge PR #6431: Compatibility of the Coq macOS package with OS X 10.11.Maxime Dénès
2017-12-15Merge PR #6219: Document undocumented optionsMaxime Dénès
2017-12-15Merge PR #6429: 8.7.1 CHANGES.Maxime Dénès
2017-12-15Compatibility of the Coq macOS package with OS X 10.11.Théo Zimmermann
2017-12-14Deprecate dead option Match Strict (ssr).Gaëtan Gilbert
2017-12-14Deprecate dead code option Congruence Depth.Gaëtan Gilbert
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-14Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...Maxime Dénès
2017-12-14Merge PR #6379: Fix profiling pluginMaxime Dénès
2017-12-14Merge PR #6422: [meta] Minor linking fix.Maxime Dénès
2017-12-14Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Maxime Dénès
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Maxime Dénès
2017-12-14Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...Maxime Dénès
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-148.7.1 CHANGES.Théo Zimmermann
2017-12-14Document Short Module Printing.Gaëtan Gilbert
2017-12-14Document Rewriting Schemes (quickly).Gaëtan Gilbert
2017-12-14Document Record Elimination Schemes.Gaëtan Gilbert
2017-12-14Document Asymmetric Patterns.Gaëtan Gilbert
2017-12-14Document some omega options (missing Omega Oldstyle).Gaëtan Gilbert
2017-12-14Add doc for Set Debug RAKAM.Gaëtan Gilbert
2017-12-14Add doc for Set Debug Cbv.Gaëtan Gilbert
2017-12-14Add doc for Set Info/Debug Auto/Trivial/Eauto.Gaëtan Gilbert
2017-12-14Add optindex for Set Bullet Behavior.Gaëtan Gilbert
2017-12-14Add doc for Set Congruence VerboseGaëtan Gilbert
2017-12-14Fix typo in doc optindex for Typeclass Resolution ...Gaëtan Gilbert
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-14Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards com...Maxime Dénès
2017-12-14Merge PR #6388: Fix issue #6387Maxime Dénès
2017-12-13Merge PR #1108: [stm] Reorganize flagsMaxime Dénès
2017-12-13Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Maxime Dénès
2017-12-13Merge PR #6251: [proof] Embed evar_map in RefinerError exception.Maxime Dénès
2017-12-13Merge 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] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-12Documenting the new options for printing "match".Hugo Herbelin
2017-12-12Decompiling pattern-matching: mini-removal dead code.Hugo Herbelin
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-12-12Improving spacing in printing disjunctive patterns.Hugo Herbelin
2017-12-12Revert "[ci] Temporal workaround for checker non-backwards compatible change."Théo Zimmermann
2017-12-12Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsMaxime Dénès
2017-12-12Further clean-up in Reductionops, removing unused lift arguments.Maxime Dénès
2017-12-12Merge PR #6359: Remove most uses of function extensionality in Program.Combin...Maxime Dénès
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-11Use msg_info for LtacProfJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:49:49 +0000