aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-12Lemmas: Little simplification of artificially convoluted code.Hugo Herbelin
2018-10-11Merge PR #8703: [vernac] Remove unused `start_hook` `save_hook` from Lemmas.Hugo Herbelin
2018-10-11Merge PR #8680: Check that lambda/prod ast's have proper binders during ↵Emilio Jesus Gallego Arias
interning/printing
2018-10-11Merge PR #8594: Miscellaneous refinements and cleaning of module printingEmilio Jesus Gallego Arias
2018-10-11Check that lambda/prod ast's have proper binders during interning/printing.Lasse Blaauwbroek
2018-10-11Merge PR #8702: [coq_dune] Abstract path operations wrt directory separator.Théo Zimmermann
2018-10-11Merge PR #8681: [dune] Fix and improve flags:Théo Zimmermann
2018-10-11Merge 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[vernac] Remove unused `start_hook` `save_hook` from Lemmas.Emilio Jesus Gallego Arias
These hooks are 10-years old and long unused I think.
2018-10-11Merge 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-11Merge PR #8699: [quote] Remove spurious file after deletion of quote plugin.Théo Zimmermann
2018-10-11Merge PR #8697: [dune] Fix public name of tool: coq_tex -> coq-texThéo Zimmermann
2018-10-11Merge PR #8648: Add minimal CHANGES entry about deprecated compat notationsThé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-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11Merge 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-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-11Merge PR #8644: [build] enable warnings on kernel/% in make based buildsMaxime Dénès
2018-10-11Merge PR #8701: Fix build of Nix package with sandbox.Vincent Laporte
2018-10-10Add minimal CHANGES entry about compat notationsJason Gross
2018-10-10Fix build of Nix package with sandbox.Théo Zimmermann
One more place where we must patch shebangs.
2018-10-10Merge 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-10Miscellaneous 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[dune] Tweaks on `tools/dune`Emilio Jesus Gallego Arias
- `coq_tex -> `coq-tex` - we build and intall `coqworkmgr` - remove some redundancy
2018-10-10Merge 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-10Merge PR #8693: [test-suite] rename a filePierre-Marie Pédrot
2018-10-10[test-suite] rename a fileVincent Laporte
2018-10-10Merge PR #8651: [dune] Provide an optimized build profile with inlining reports.Pierre-Marie Pédrot
2018-10-10Merge PR #6218: Fix #5197, handling of algebraic universesPierre-Marie Pédrot
2018-10-10Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit ↵Enrico Tassi
tests.
2018-10-10Merge PR #8679: [test suite] Compile test cases, instead of only loading themEnrico Tassi
2018-10-10Merge PR #8457: Refactoring of Micromega plugin (including new Simplex based ↵Vincent Laporte
solver)
2018-10-09Merge 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-suiteVincent Laporte
2018-10-09[test-suite] use “-async-proofs-cache force” when compilingVincent Laporte
2018-10-09[default.nix] some fixesVincent 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 casesVincent Laporte
2018-10-09[test-suite] ensure file names are valid module namesVincent Laporte
2018-10-09Refactoring of Micromega code using a Simplex linear solverFré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-09Merge PR #8632: [ide] [dune] [test-suite] Reorganize `fake_ide` build.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 14:08:44 +0000