aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-12-27Fix #5998: AppVeyor package building is currently failingMaxime Dénès
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
(fix #6106)
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 ↵Maxime Dénès
same right-hand side.
2017-12-14Merge PR #6373: Further clean-up in Reductionops, removing unused lift ↵Maxime Dénès
arguments.
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
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 ↵Maxime Dénès
compatible change.
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 ↵Maxime Dénès
`make clean`.
2017-12-13[meta] Minor linking fix.Emilio Jesus Gallego Arias
2017-12-12Documenting the new options for printing "match".Hugo Herbelin
Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause.
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
Moreover, when there are at least two clauses and the last most factorizable one is a disjunction with no variables, turn it into a catch-all clause. Adding options Unset Printing Allow Default Clause. to deactivate the second behavior, and Unset Printing Factorizable Match Patterns. to deactivate the first behavior (deactivating the first one deactivates also the second one). E.g. printing match x with Eq => 1 | _ => 0 end gives match x with | Eq => 1 | _ => 0 end or (with default clause deactivates): match x with | Eq => 1 | Lt | Gt => 0 end More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
This is to have a better symmetry between CCases and GCases.
2017-12-12Improving spacing in printing disjunctive patterns.Hugo Herbelin
Adding a space before the bar separating disjunctive patterns. Removing an extra space after the bar for inner disjunctive patterns.
2017-12-12Revert "[ci] Temporal workaround for checker non-backwards compatible change."Théo Zimmermann
This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f.
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
This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2.
2017-12-12Merge PR #6359: Remove most uses of function extensionality in ↵Maxime Dénès
Program.Combinators
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-11Use msg_info for LtacProfJason Gross
This way, `Time Show Ltac Profile` shows the profile in `*response*` in PG, without an extra `infomsg` tag on the timing.
2017-12-11Allow LtacProf tactics to be calledJason Gross
This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer.
2017-12-11Merge PR #6312: [configure] fix detection of `md5sum`Maxime Dénès
2017-12-11Catch errors while coercing 'and' intro patternsTej Chajed
Fixes GH#6384 and GH#6385.
2017-12-11Fix issue #6387Martin Vassor
2017-12-11Merge PR #6331: Linter: skip PRs older than the linter.Maxime Dénès
2017-12-11Merge PR #6311: Don't Add LoadPath on CoqIDE startup, #6153Maxime Dénès
2017-12-11Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.Maxime Dénès
2017-12-11Fix 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
The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair.
2017-12-11Restoring filtering of native files passed to `rm` during `make clean`.Maxime Dénès
Was lost during the coq_makefile 1 -> 2 translation.
2017-12-11Add overlay.Théo Zimmermann
2017-12-11Remove deprecated appcontext and corresponding documentation.Théo Zimmermann
2017-12-11Remove deprecated option Tactic Compat Context.Théo Zimmermann
And some code simplification.
2017-12-11Remove deprecated option Dependent Propositions Eliminiation.Théo Zimmermann
And a bit of code simplification.
2017-12-11[flags] [stm] Reorganize flags.Emilio Jesus Gallego Arias
We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
2017-12-11[stm] Move process_id to Spawned.Emilio Jesus Gallego Arias
This brings us one step closer to actually moving all STM flags to `stm`.
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-11Merge PR #6352: [makefile] Address #6291: install more development files.Maxime Dénès
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-11Merge PR #1150: [stm] Remove all but one use of VtUnknown.Maxime Dénès
2017-12-11Merge PR #6338: Remove up-to-conversion term matchingMaxime Dénès
2017-12-11Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 08:52:31 +0000