| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-18 | Merge PR #9178: CoqIDE: Restoring configuration of default width/height of ↵ | Pierre-Marie Pédrot | |
| main window. | |||
| 2018-12-18 | Merge PR #9215: Set up CI with Azure Pipelines | Emilio Jesus Gallego Arias | |
| 2018-12-17 | Merge PR #9153: [api] Move reduction modules to `tactics` | Pierre-Marie Pédrot | |
| 2018-12-17 | [STM] Better protection for cur_id | Maxime Dénès | |
| Since some state handling refactoring, `purify_stm` was no longer protecting against assignement of cur_id, resulting in confusing behavior w.r.t. cache. | |||
| 2018-12-17 | Merge PR #9238: CI: simple-io now depends on ext-lib | Emilio Jesus Gallego Arias | |
| 2018-12-17 | Set up CI with Azure Pipelines | Gaëtan Gilbert | |
| 2018-12-17 | simple-io now depends on ext-lib | Gaëtan Gilbert | |
| 2018-12-17 | Merge PR #8856: [gitlab] Test Ocaml trunk. | Gaëtan Gilbert | |
| 2018-12-17 | Restrict body universes in delayed mode. | Gaëtan Gilbert | |
| 2018-12-17 | Fix git line ending conversion in windows | Gaëtan Gilbert | |
| 2018-12-17 | Stop printing Monomorphic/Polymorphic in Print. | Gaëtan Gilbert | |
| You can tell which it is from the `@{}` if you really care, and seeing `Monomorphic List (A:Type)` with no indication that `Monomorphic` is about universes can confuse people. | |||
| 2018-12-17 | Remove universe specific terminology from acyclicgraph | Gaëtan Gilbert | |
| This means removing [univ], [level] and derived abbreviations like [lvl]. We keep using u, v for variable names as doing otherwise would be too intrusive, and it's not overly universe specific. | |||
| 2018-12-17 | Make ugraph implementation abstract wrt universe specifics | Gaëtan Gilbert | |
| This should give better visibility of universe specific operations vs generic graph operations. | |||
| 2018-12-17 | Add Map.find_opt | Gaëtan Gilbert | |
| 2018-12-17 | Fix classification of Set Default Proof Mode. | Gaëtan Gilbert | |
| 2018-12-17 | Merge PR #9206: [stm] join the tip of the document even when fixing a proof ↵ | Emilio Jesus Gallego Arias | |
| (fix #9204) | |||
| 2018-12-17 | Merge PR #9219: [STM] Fix logic of debug DAG printer | Enrico Tassi | |
| 2018-12-17 | Merge PR #9220: Move shallow state logic to the function preparing state for ↵ | Enrico Tassi | |
| workers | |||
| 2018-12-17 | CoqIDE: Restoring configuration of default width/height of main window. | Hugo Herbelin | |
| Also removing dead code about show_toolbar: this is governed by an item of the view menu rather than by the preference panel since aa357d601 (Dec 2003). | |||
| 2018-12-16 | Merge pull request coq/ltac2#91 from ejgallego/proof_rework | Pierre-Marie Pédrot | |
| [coq] Adapt to coq/coq#9172 | |||
| 2018-12-16 | Merge PR #9172: [proof] Rework proof interface. | Pierre-Marie Pédrot | |
| 2018-12-15 | Avoid explicit names in binders for automatic intros | Jasper Hugunin | |
| 2018-12-14 | Merge PR #9073: [sphinx] No more undocumented objects. | Clément Pit-Claudel | |
| 2018-12-14 | Fix issue: Windows CI: cygwin install cache is not reused #9212 | Michael Soegtrop | |
| 2018-12-14 | [dune] [gitlab] Test OCaml trunk. | Emilio Jesus Gallego Arias | |
| We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too. | |||
| 2018-12-14 | Merge PR #9147: [dune] [doc] Support for building the reference manual with ↵ | Théo Zimmermann | |
| Dune. | |||
| 2018-12-14 | [proof] Rework proof interface. | Emilio Jesus Gallego Arias | |
| - deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways. | |||
| 2018-12-14 | Update pinned nixpkgs to use Dune 1.6. | Théo Zimmermann | |
| 2018-12-14 | Turn warning on for undocumented objects. Closes #7602. | Théo Zimmermann | |
| 2018-12-14 | Fix the SSReflect chapter regarding objects without bodies. | Théo Zimmermann | |
| 2018-12-14 | Do not raise object without body warning for prodn objects. | Théo Zimmermann | |
| 2018-12-13 | Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost ↵ | Gaëtan Gilbert | |
| of evars in shelf) | |||
| 2018-12-13 | Merge PR #9194: Fixing uses of sed in #8985 which do not work on MacOS X | Matthieu Sozeau | |
| 2018-12-13 | Fixing uses of sed which do not work on MacOS X. | Hugo Herbelin | |
| This was introduced in PR #8985. | |||
| 2018-12-13 | Merge PR #9117: Accept argument names for extra arguments with "extra scopes" | Matthieu Sozeau | |
| 2018-12-13 | Add overlay | Maxime Dénès | |
| 2018-12-13 | Merge PR #9210: Fix issue #9176 : Windows: change cygwin repo | Théo Zimmermann | |
| 2018-12-13 | Merge PR #9211: Fixing incorrect mention of coercions as being part of the ↵ | Théo Zimmermann | |
| interning phase | |||
| 2018-12-13 | [dune] [doc] Support for building the reference manual with Dune. | Emilio Jesus Gallego Arias | |
| This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted. | |||
| 2018-12-13 | [engine] Allow debug printers to access the environment. | Emilio Jesus Gallego Arias | |
| This should improve correctness and will be needed for the PRs that remove global access to the proof state. | |||
| 2018-12-13 | Merge PR #9032: checker: check inductive types by roundtrip through the kernel. | Pierre-Marie Pédrot | |
| 2018-12-13 | Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as ↵ | Pierre-Marie Pédrot | |
| pattern variables | |||
| 2018-12-13 | Merge PR #9169: [rtauto] [auto] Use new proof engine. | Pierre-Marie Pédrot | |
| 2018-12-13 | Merge PR #9217: [ci] [appveyor] Temporally disable test suite on Appveyor. | Gaëtan Gilbert | |
| 2018-12-13 | [test] for join when error resiliency on and async-proofs off | Enrico Tassi | |
| 2018-12-13 | [stm] join: check no error states are part of the document | Enrico Tassi | |
| The error-resiliency feature may have managed to reach the end of the document by recovering some error | |||
| 2018-12-13 | Merge PR #9196: Document the deprecation of hint declaration withou database ↵ | Maxime Dénès | |
| in refman. | |||
| 2018-12-13 | [test] for #9204 | Enrico Tassi | |
| 2018-12-13 | [stm] join the tip of the document even when fixing a proof (fix #9204) | Enrico Tassi | |
| 2018-12-13 | Move shallow state logic to the function preparing state for workers | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |