| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-11 | Documenting -arg in _CoqProject. | Hugo Herbelin | |
| We follow Proof General documentation, section 11.2 "Using the Coq project file". | |||
| 2018-10-11 | Merge PR #8702: [coq_dune] Abstract path operations wrt directory separator. | Théo Zimmermann | |
| 2018-10-11 | Merge PR #8681: [dune] Fix and improve flags: | Théo Zimmermann | |
| 2018-10-11 | Merge PR #8566: [dune] [test-suite] Support for running the test suite with ↵ | Théo Zimmermann | |
| Dune. | |||
| 2018-10-11 | [coq_dune] Abstract path operations wrt directory separator. | Emilio Jesus Gallego Arias | |
| Even if cosmetic, this is useful for window-based hosts. | |||
| 2018-10-11 | Merge PR #8698: [dune] Require that `plugin_base.dune` exists in plugin dirs. | Théo Zimmermann | |
| 2018-10-11 | [dune] Add optimizing flags to release profile. | Emilio Jesus Gallego Arias | |
| - In `release` profile, we use an optimizing set of flags. This will only affect to people using a Flambda-enabled OCaml. - We use the `_` pattern for flags that are common to all profiles. | |||
| 2018-10-11 | Merge PR #8699: [quote] Remove spurious file after deletion of quote plugin. | Théo Zimmermann | |
| 2018-10-11 | Merge PR #8697: [dune] Fix public name of tool: coq_tex -> coq-tex | Théo Zimmermann | |
| 2018-10-11 | Merge PR #8648: Add minimal CHANGES entry about deprecated compat notations | Théo Zimmermann | |
| 2018-10-11 | [dune] [test-suite] Support for running the test suite with Dune. | Emilio Jesus Gallego Arias | |
| 2018-10-11 | [configure] Use absolute path for prefix. | Emilio Jesus Gallego Arias | |
| 2018-10-11 | Merge PR #186: [RFC] Coqlib cleanup | Pierre-Marie Pédrot | |
| 2018-10-11 | Merge PR #8709: [test-suite] Use the right OCAMLPATH separator on Windows. | Vincent Laporte | |
| 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-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 | [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 | [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 | 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |