aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-12-19Fix typo in the refman.Théo Zimmermann
2017-12-19Merge PR #6400: Circle CIMaxime Dénès
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-18Merge PR #6447: [make] More build fixes for static plugins and ocamlfind.Maxime Dénès
2017-12-18Merge PR #6284: Warning for absolute name masking (deprecated, should become ↵Maxime Dénès
an error)
2017-12-18Merge PR #6381: A version of [time] that works on constr evaluationMaxime Dénès
2017-12-18Merge PR #6406: Make [abstract] nodes show up in the Ltac profileMaxime Dénès
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Maxime Dénès
Extraction Language command
2017-12-18Merge PR #6305: Build with windows line endingsMaxime Dénès
2017-12-18Merge PR #6217: Do dependencies in 1 command per file class.Maxime Dénès
2017-12-18Merge PR #6453: [doc] Nit on the manual.Maxime Dénès
2017-12-18Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingMaxime Dénès
2017-12-18Merge PR #6419: [vernac] Split `command.ml` into separate files.Maxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
This is useful as it allows to reflect program_mode behavior as an attribute.
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413.
2017-12-17[doc] Nit on the manual.Emilio Jesus Gallego Arias
`ssrnat` is mentioned, but it is not distributed with Coq.
2017-12-16Fix build fileJim
2017-12-16For bug 6249, Segmentation fault when building Coq on Windows 10.Jim
Enable builds on Windows by removing Windows-style endings where it impacts make. The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here.
2017-12-16[make] More build fixes for static plugins and ocamlfind.Emilio Jesus Gallego Arias
- In ocamlfind-based byte builds, link the VM statically as in native builds. This is the best way to get reliable, path-independent self-contained executables. - In `make install`, install the `.cmx` files for plugins too. To statically link Coq plugins in native mode, both the `.cmx` and `.o` files must be present.
2017-12-15Overlay for unimath.Gaëtan Gilbert
2017-12-15Do dependencies in 1 command per file class.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-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
2017-12-15Fix #5368: Canonical structure unification fails.Pierre-Marie Pédrot
Universe instances were lost during constructions of the canonical instance.
2017-12-15Compatibility of the Coq macOS package with OS X 10.11.Théo Zimmermann
Travis has moved on to macOS 10.12 but this makes the package incompatible with earlier versions. This fix should restore the compatibility with OS X 10.11.
2017-12-14Pass a ghost location for abstractJason Gross
As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902
2017-12-14Make [abstract] nodes show up in the Ltac profileJason Gross
This closes #5082 and closes #5778, but makes #6404 apply to `abstract` as well as `transparent_abstract`. This is unfortunate, but I think it is worth it to get `abstract` in the profile (and therefore not misassign the time spent sending the subproof to the kernel). Another alternative would have been to add a dedicated entry to `ltac_call_kind` for `TacAbstract`, but I think it's better to just deal with #6404 all at once. The "better" solution here would have been to move `abstract` out of the Ltac syntax tree and define it via `TACTIC EXTEND` like `transparent_abstract`. However, the STM relies on its ability to recognize `abstract` and `solve [ abstract ... ]` syntactically so that it can handle `par: abstract`. Note that had to add locations to `TacAbstract` nodes, as I could not figure out how to call `push_trace` otherwise.
2017-12-14Add documentation for time_constrJason Gross
2017-12-14Deprecate dead option Match Strict (ssr).Gaëtan Gilbert
2017-12-14Deprecate dead code option Congruence Depth.Gaëtan Gilbert
2017-12-14Add named timers to LtacProfJason Gross
I'm not sure if they belong in profile_ltac, or in extratactics, or, perhaps, in a separate plugin. But I'd find it very useful to have a version of `time` that works on constr evaluation, which is what this commit provides. I'm not sure that I've picked good naming conventions for the tactics, either.
2017-12-14Add doc+changelog entries for new LtacProf tacticsJason Gross
2017-12-14Add tactics to reset and display the Ltac profileJason Gross
This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:47:19 +0000