| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-26 | Merge PR #885: Removing a dummy parameter in some FMapPositive statements. | Maxime Dénès | |
| 2017-07-26 | Merge PR #868: Fix debug trace of typeclasses eauto. | Maxime Dénès | |
| 2017-07-26 | Merge PR #845: Add Z.mod_div lemma to standard library. | Maxime Dénès | |
| 2017-07-26 | Merge PR #905: [api] Remove type equalities from API. | Maxime Dénès | |
| 2017-07-26 | Merge PR #857: Extraction: various fixes related with bug 4720 | Maxime Dénès | |
| 2017-07-26 | Merge PR #859: Extraction TestCompile | Maxime Dénès | |
| 2017-07-26 | Merge PR #808: [api] Put some order in API.mli | Maxime Dénès | |
| 2017-07-26 | Merge PR #750: Remove deprecated options of ./configure in 8.8 | Maxime Dénès | |
| 2017-07-26 | make sure that API-leaks cannot be reintroduced by mistake | Matej Košík | |
| 2017-07-25 | Makefile.ide: restore a coqide-binaries rule (fix bug 5667) | Pierre Letouzey | |
| This rule is used by opam package coq-coqide | |||
| 2017-07-25 | [api] Remove type equalities from API. | Emilio Jesus Gallego Arias | |
| This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli` | |||
| 2017-07-25 | [api] Put modules in order in API.{mli,ml} | Emilio Jesus Gallego Arias | |
| We sort the dependency graph of API by following a logical declaration order in `API.{ml,mli}` related to the actual dependency order of Coq modules. Things are a bit tricky here as Coq itself relies on the fact that OCaml treats module interface and implementation separately dependency-wise; however, when resorting module alias the design seems to become more coupled. Currently, API exposes both "namespaces", asserting a large number of type equality between them, however the `API` namespace is not self-contained. In particular, this is a first step to solve problems such as `Summary.frozen` being used in `API.mli` but not declared by the `API.Summary` module, etc... In general we follow the invariant that a type used in `API` must have been declared before. Keep in mind that OCaml upstream has warned that it maybe tricky to alias objects in this way. In particular, after API the old `mli` only files have become full compilation units so we may want to be more careful here. The more "correct" declaration order allows us to remove the `API.Prelude` module, as well as some other declarations that I consider as spurious. We still maintain the large number of type aliases which will be removed in a future patch. We follow linking order except for files in `intf`, which are conceptually wrongly placed in the linking hierarchy but this doesn't matter as the files don't contain any implementation. We also move a couple of `.mli` only files to `.ml` so we are consistent, and correct their linking order in `mllib`, even if that doesn't matter as such `.ml`-only files contain no implementations. | |||
| 2017-07-21 | Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile) | Maxime Dénès | |
| 2017-07-21 | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it. | Maxime Dénès | |
| 2017-07-21 | Install time command under Cygwin (required for timing scripts). | Maxime Dénès | |
| 2017-07-20 | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720) | Pierre Letouzey | |
| Avoid Anomaly (or Assert False) when a module signature contains an applied functor followed by a "with Definition" or "with Module" Also fix the dependency computation in presence of a "with Definition" Concerning 4720, the code extracted out of this bug report was suboptimal in Coq 8.4 (it was compilable, but could have probably been tweaked into a real issue producing faulty code). But the example of 4720 (and some variants of it) was broken since 8.5, for the same reasons as 5177 and 5240. And the good news is that after these repairs, the example of bug 4720 is now extracted to correct code (the "with" is preserved). | |||
| 2017-07-20 | Merge PR #892: Improve do_split option of typeclass resolution | Maxime Dénès | |
| 2017-07-20 | fake_ide: do as coqide to find out coqtop path | Enrico Tassi | |
| 2017-07-20 | coq_makefile: use System.exists_dir for better portability | Enrico Tassi | |
| 2017-07-20 | Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash) | Enrico Tassi | |
| 2017-07-20 | coq-makefile: strip windows drive letter when DESTDIR is not empty | Enrico Tassi | |
| In unix one can concatenate a prefix with an absolute path in order to obtain a valid path. This is not the case on Windows. | |||
| 2017-07-20 | coq-makefile: treat coq_makefile as any other coq binary | Enrico Tassi | |
| In particular, find it under $(COQBIN) | |||
| 2017-07-20 | more verbose logs for coq-makefile | Enrico Tassi | |
| 2017-07-20 | coq-makefile: quote using ' to preserve \ (windows paths) | Enrico Tassi | |
| 2017-07-20 | coq-makefile: make test suite detect more errors | Enrico Tassi | |
| Replacing ; with && and enabling bash's pipefail option | |||
| 2017-07-20 | In fake_ide, call coqtop.exe instead of coqtop on Win32. | Maxime Dénès | |
| 2017-07-20 | Avoid using unsupported signals under Windows in fake_ide. | Maxime Dénès | |
| 2017-07-20 | Remove trailing CR before diff in output and misc tests. | Maxime Dénès | |
| 2017-07-20 | Print failure logs on appveyor. | Maxime Dénès | |
| 2017-07-20 | Remove non-terminating Timeout tests from Hints.v. | Maxime Dénès | |
| 2017-07-20 | Make coqlib relative in test suite (revert 024a7ab20b0) | Maxime Dénès | |
| 2017-07-20 | Add AppVeyor infrastructure, launching the test suite under Windows. | Maxime Dénès | |
| 2017-07-20 | Merge PR #900: [proofs] Remove circular dependency from Proofview to Goal. | Maxime Dénès | |
| 2017-07-20 | Merge PR #899: [general] Move files to directories so they match linking order. | Maxime Dénès | |
| 2017-07-20 | Merge PR #903: Documenting the purity / marshallability invariant of ↵ | Maxime Dénès | |
| persistent states. | |||
| 2017-07-20 | Documenting the purity / marshallability invariant of persistent states. | Pierre-Marie Pédrot | |
| 2017-07-20 | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Maxime Dénès | |
| 2017-07-20 | Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker | Maxime Dénès | |
| 2017-07-20 | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | |
| 2017-07-20 | Merge PR #877: Travis+4.05.0 | Maxime Dénès | |
| 2017-07-20 | Merge branch 'v8.7' | Maxime Dénès | |
| 2017-07-19 | Merge PR #745: Add timing scripts | Maxime Dénès | |
| 2017-07-19 | Merge PR #855: Deprecate options that were introduced for compatibility with ↵ | Maxime Dénès | |
| 8.5. | |||
| 2017-07-19 | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | |
| 2017-07-19 | [proofs] Remove circular dependency from Proofview to Goal. | Emilio Jesus Gallego Arias | |
| 2017-07-19 | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias | |
| We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. | |||
| 2017-07-19 | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | Maxime Dénès | |
| 2017-07-19 | [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | Emilio Jesus Gallego Arias | |
| Fix bug introduced by a Haskell programmer. | |||
| 2017-07-19 | Fix debug trace of typeclasses eauto. | Théo Zimmermann | |
| 2017-07-19 | Fixing the checker w.r.t. wrongly used abstract universe contexts. | Pierre-Marie Pédrot | |
| It seems we were not testing the checker on cumulative inductive types, because judging from the code, it would just have exploded in anomalies. Before this patch, the checker was mixing De Bruijn indices with named variables, resulting in ill-formed universe contexts used throughout the checking of cumulative inductive types. This patch also gets rid of a lot of now dead code, and removes abstraction breaking code from the checker. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |