| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-11 | The cbv reduction does not rely on the kernel info data structure anymore. | Pierre-Marie Pédrot | |
| 2018-10-11 | Stupid but critical unfolding heuristic. | Pierre-Marie Pédrot | |
| We favour unfolding of variables over constants because it is more frequent for the former to depend on the latter. This has huge consequences on a few extremely slow lines in mathcomp, up to dividing by 3 single-line invocations that were taking about 30s on my laptop before the patch. | |||
| 2018-10-11 | [test-suite] Use the right OCAMLPATH separator on Windows. | Emilio Jesus Gallego Arias | |
| Hopefully this goes away when OCAMLPATH is properly handled by the build system. | |||
| 2018-10-11 | Merge PR #8161: Implement VERNAC EXTEND in coqpp | Maxime Dénès | |
| 2018-10-11 | Merge PR #8644: [build] enable warnings on kernel/% in make based builds | Maxime Dénès | |
| 2018-10-11 | Merge PR #8701: Fix build of Nix package with sandbox. | Vincent Laporte | |
| 2018-10-11 | [coq] Adapt for PR #8704. | Emilio Jesus Gallego Arias | |
| 2018-10-10 | Add minimal CHANGES entry about compat notations | Jason Gross | |
| 2018-10-10 | Fix build of Nix package with sandbox. | Théo Zimmermann | |
| One more place where we must patch shebangs. | |||
| 2018-10-10 | Merge PR #8384: Small fixes in attribute documentation. | Clément Pit-Claudel | |
| 2018-10-10 | [quote] Remove spurious file after deletion of quote plugin. | Emilio Jesus Gallego Arias | |
| For some reason PR #7894 left this spurious file; this is typical of a bad resolution of a merge, and while the file is innocuous it should go away. | |||
| 2018-10-10 | Miscellaneous refinements/cleaning of module printing. | Hugo Herbelin | |
| This refines the fix to #2169 by distinguishing the short and non-short printing modes. This prepares functionalization of printers by always passing env rather than setting env to None in short mode. This is not strictly necessary for the env which is not used for printing global references but it shall be more consistent in style when passing e.g. the nametab functionally. We however keep the fallback printer used in case of error while printing: due to missing registration of submodule fields in the nametab, printing with types does not work if there are references to an inner module. | |||
| 2018-10-10 | [dune] Require that `plugin_base.dune` exists in plugin dirs. | Emilio Jesus Gallego Arias | |
| `coq_dune` should not consider a directory as a plugin one if the `plugin_base.dune` file doesn't exists, as the generated `dune` file for that dir will try to include it. We have had problems with this in the past due to spurious dirs. | |||
| 2018-10-10 | [doc] [sphinx] Fix title levels. | Théo Zimmermann | |
| 2018-10-10 | Include all menu entries in the menu/short TOC so that users can view | Jim Fehrle | |
| menu options for all chapters without having to load a new chapter. Change "Introcution" title to "Introduction and Contents" | |||
| 2018-10-10 | Fix names for 2 entries in Flags, Options, Tables index. | Jim Fehrle | |
| 2018-10-10 | [dune] Tweaks on `tools/dune` | Emilio Jesus Gallego Arias | |
| - `coq_tex -> `coq-tex` - we build and intall `coqworkmgr` - remove some redundancy | |||
| 2018-10-10 | Merge PR #8692: [test-suite] Don't reset `OCAMLPATH`, but append to it. | Enrico Tassi | |
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias | |
| We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2018-10-10 | [test-suite] Don't reset `OCAMLPATH`, but append to it. | Emilio Jesus Gallego Arias | |
| This fixes an obvious bug introduced in #8602. | |||
| 2018-10-10 | Merge PR #8693: [test-suite] rename a file | Pierre-Marie Pédrot | |
| 2018-10-10 | [test-suite] rename a file | Vincent Laporte | |
| 2018-10-10 | Merge PR #8651: [dune] Provide an optimized build profile with inlining reports. | Pierre-Marie Pédrot | |
| 2018-10-10 | Merge PR #6218: Fix #5197, handling of algebraic universes | Pierre-Marie Pédrot | |
| 2018-10-10 | Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit ↵ | Enrico Tassi | |
| tests. | |||
| 2018-10-10 | Merge PR #8679: [test suite] Compile test cases, instead of only loading them | Enrico Tassi | |
| 2018-10-10 | Merge PR #8457: Refactoring of Micromega plugin (including new Simplex based ↵ | Vincent Laporte | |
| solver) | |||
| 2018-10-09 | Merge PR #8673: Remove dead code in universe handling in the abstract tactical. | Gaëtan Gilbert | |
| 2018-10-09 | [dune] Provide an optimized build profile with inlining reports. | Emilio Jesus Gallego Arias | |
| This satisfies a wish by @ppedrot | |||
| 2018-10-09 | [default.nix] Add install dir to OCAMLPATH before running the test-suite | Vincent Laporte | |
| 2018-10-09 | [test-suite] use “-async-proofs-cache force” when compiling | Vincent Laporte | |
| 2018-10-09 | [default.nix] some fixes | Vincent Laporte | |
| 2018-10-09 | [test-suite] Use ocamlfind to locate Coq libraries in unit tests. | Emilio Jesus Gallego Arias | |
| This is slightly more robust and allows to run the test suite with Dune which may place OCaml objects differently. | |||
| 2018-10-09 | [test-suite] compile (rather than load) test cases | Vincent Laporte | |
| 2018-10-09 | [test-suite] ensure file names are valid module names | Vincent Laporte | |
| 2018-10-09 | [coqchk] Fix checking of records in module signatures | Vincent Laporte | |
| 2018-10-09 | Simplify code for [Definition := Eval ...] | Gaëtan Gilbert | |
| Note that since this now reduces before restricting universes behaviour may be a bit different. | |||
| 2018-10-09 | Fix nativenorm when an evar is in the wrong place. | Gaëtan Gilbert | |
| See commit [Simplify code for [Definition := Eval ...]] which without this breaks test suite 7631.v | |||
| 2018-10-09 | [coqchk] Fix checking of inductive types | Vincent Laporte | |
| 2018-10-09 | [coqchk] Fix case_info for primitive records | Vincent Laporte | |
| 2018-10-09 | [coqchk] Fix subterm relation for primitive projections | Vincent Laporte | |
| 2018-10-09 | [coqchk] Fix guard condition with commutative cuts | Vincent Laporte | |
| 2018-10-09 | Refactoring of Micromega code using a Simplex linear solver | Frédéric Besson | |
| - Simplex based linear prover Unset Simplex to get Fourier elimination For lia and nia, do not enumerate but generate cutting planes. - Better non-linear support Factorisation of the non-linear pre-processing Careful handling of equation x=e, x is only eliminated if x is used linearly - More opaque interfaces (Linear solvers Simplex and Mfourier are independent) - Set Dump Arith "file" so that lia,nia calls generate Coq goals in filexxx.v. Used to collect benchmarks and regressions. - Rationalise the test-suite example.v only tests psatz Z example_nia.v only tests lia, nia In both files, the tests are in essence the same. In particular, if a test is solved by psatz but not by nia, we finish the goal by an explicit Abort. There are additional tests in example_nia.v which require specific integer reasoning out of scope of psatz. | |||
| 2018-10-09 | Merge PR #8632: [ide] [dune] [test-suite] Reorganize `fake_ide` build. | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8676: Fixes #8672: ill-formed pattern substitution in notation ↵ | Emilio Jesus Gallego Arias | |
| with "let" | |||
| 2018-10-08 | Merge PR #8674: [ci] Add aac-tactics. | Emilio Jesus Gallego Arias | |
| 2018-10-08 | Fixes #8672 (ill-formed pattern substitution in notation with "let"). | Hugo Herbelin | |
| 2018-10-08 | [ide] [dune] [test-suite] Reorganize `fake_ide` build. | Emilio Jesus Gallego Arias | |
| Even if `fake_ide` was under tools, it depended on libraries from `ide`. Thus, we move `fake_ide` to `ide`, and make it "private" to the test-suite [this means `test-suite` depends on the `ide` folder then]. In the Dune side, we reorganize libraries so `fake_ide` doesn't depend on GTK anymore, this allows to run the test-suite when GTK is not available. In order to achieve this, we had to split the `coqide` package in a server and client version. | |||
| 2018-10-08 | [ci] Add aac-tactics. | Théo Zimmermann | |
| And fix a typo that was previously there. | |||
| 2018-10-08 | Merge PR #8677: [dune] Fix bad interaction among PR #8627 and #8657 | Maxime Dénès | |
