aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-14Vm_compute: taking into account let-ins in parameters of constructors.Hugo Herbelin
2017-12-14Cosmetic: using "types" rather "constr" in some types of term.mli.Hugo Herbelin
This enforces the intended meaning of the corresponding functions (prod_appvect*/prod_applist*).
2017-12-14Fixing a bug of Print for inductive types with let-ins in parameters.Hugo Herbelin
Adding a "let-in"-sensitive function hnf_prod_applist_assum to instantiate parameters and using it for printing. Thanks to PMP for reporting.
2017-12-14Fixes incorrect anomaly message in lambda/prod_applist_assum + typo in doc.Hugo Herbelin
Was introduced in e8c47b65.
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-14Circle CI: add badge to README.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-14Circle CI: separate job to boot opam with all used packages.Gaëtan Gilbert
2017-12-14Circle CI: remove warning jobsGaëtan Gilbert
2017-12-14Circle CI: cat failed test suite logsGaë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 ↵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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 22:12:43 +0000