| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-10-08 | [dune] Fix bad interaction among PR #8627 and #8657 | Emilio Jesus Gallego Arias | |
| Dangers of not stacking PRs hit again, and here we hit a problem breaking the build on master due to #8627 adding a new file to install with for the (implicit) `coq` package and #8657 removing the implicit status of such package. | |||
| 2018-10-08 | Merge PR #8657: [dune] Refactor files following advice from upstream. | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8654: Remove FCast from CClosure.fterm. | Maxime Dénès | |
| 2018-10-08 | Fix #5197, handling of algebraic universes | Matthieu Sozeau | |
| They were allowed to stay in terms in some cases. We now ensure that if an evar is defined as e.g. fun x => Type@{foo}, foo is properly refreshed to be non-algebraic as it could otherwise appear in the term and break the invariant. Also cleanup the implementation of refresh_universes to avoid using a mutable reference and simply rely on the Constr.map smartmap idiom instead. This might have compatibility issues, e.g. in HoTT where maybe more non-algebraic proxy universes could be generated, we'll see. For the bug report proper, there is a lack of bidirectional type-checking that makes the initial definition fail (there's a non-canonical choice of dependency if we don't consider the typing constraint). With the Program bidir hint it passes. | |||
| 2018-10-08 | Remove dead code in universe handling in the abstract tactical. | Pierre-Marie Pédrot | |
| Since 213b323 the kernel was expecting to receive an empty set of internal universe constraints in polymorphic definitions. We lift this invariant to the code that actually generates side effects. | |||
| 2018-10-08 | Merge PR #8660: Issue 8659 not always build all addons | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune. | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8585: Simplify declaration of universe names | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8668: Missing headers in two files | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8630: Some cleaning in the test suite | Enrico Tassi | |
| 2018-10-08 | Merge remote-tracking branch 'remotes/origin/pr/74' | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8554: Fixes #8553: regression of tactic "change" under binders. | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8582: [api] Deprecate `evar_map` ref combinators. | Pierre-Marie Pédrot | |
| 2018-10-07 | Adding missing header in functional_principles_types.ml. | Hugo Herbelin | |
| 2018-10-07 | Adding missing header to comFixpoint.ml. | Hugo Herbelin | |
| 2018-10-07 | [api] Deprecate `evar_map` ref combinators. | Emilio Jesus Gallego Arias | |
| All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the combinators to discourage this style of programming. Still a few places do use imperative style, but they are pretty localized and should be cleaned up separately. As these are the last bits of `e_` API remaining this PR closes #6342. | |||
| 2018-10-07 | Merge PR #8493: [api] Remove (most) 8.9 deprecated objects. | Pierre-Marie Pédrot | |
| 2018-10-06 | Merge PR #7850: Rewrite CEphemeron to use a type-safe implementation based ↵ | Pierre-Marie Pédrot | |
| on GADTs | |||
| 2018-10-06 | Merge remote-tracking branch 'maximedenes/rm-section-path' | Pierre-Marie Pédrot | |
| 2018-10-06 | [api] Remove (most) 8.9 deprecated objects. | Emilio Jesus Gallego Arias | |
| A few of them will be of help for future cleanups. We have spared the stuff in `Names` due to bad organization of this module following the split from `Term`, which really difficult things removing the constructors. | |||
| 2018-10-06 | Merge PR #8555: Remove section paths from kernel names | Pierre-Marie Pédrot | |
| 2018-10-05 | Merge PR #8662: Fix printing of raw terms for lambda's without parameters ↵ | Emilio Jesus Gallego Arias | |
| (continued, adding smart constr_expr binder constructors) | |||
| 2018-10-05 | [ci] Allow bedrock2 to fail. | Emilio Jesus Gallego Arias | |
| Issue #8533 is still unmitigated. | |||
| 2018-10-05 | Merge PR #8658: Remove duplicate committers. | Théo Zimmermann | |
| 2018-10-05 | Merge PR #8645: Improve markdown in changes. | Théo Zimmermann | |
| 2018-10-05 | [dune] Refactor files following advice from upstream. | Emilio Jesus Gallego Arias | |
| After some discussion upstream, I think that for the current a multi-package setup in a single repository this setup saves a bit work. The most problematic bit is the `-rectypes` flag; its status is not saved per-library so we must either duplicate the flags in the coqide scope (scope == dune-project file), or unify its scope with Coq. We do this last option as this seems like the easiest thing for now. Changes: - Move coqide.opam file to the root, use a single scope/`dune-project` file. - Remove `dune-workspace`, this should be owned by the developer / user. | |||
| 2018-10-05 | Merge PR #8661: CI: fix Iris and stdpp ref selection | Emilio Jesus Gallego Arias | |
| 2018-10-05 | Fix review requests | Michael Soegtrop | |
| 2018-10-05 | Remove old folder delete (can interfere with unique folder creation) | Michael Soegtrop | |
| 2018-10-05 | Fix issue #8659 - Not always build extended set of addons for Windows installer | Michael Soegtrop | |
| 2018-10-05 | Merge PR #8650: [ci] [dune] [opam] Fixes to OPAM and CI target. | Gaëtan Gilbert | |
| 2018-10-05 | CI: fix Iris and stdpp ref selection | Gaëtan Gilbert | |
| This was broken due to a typo when introducing the archive download method. We also remove default [master] values from basic-overlay which hid this issue. | |||
| 2018-10-05 | Using smart mkLambdaCN/mkProdCN. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |