aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18Merge PR #9218: [STM] Better protection for cur_idEnrico Tassi
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-18Merge PR #9160: Avoid user-given names in automatic introduction of bindersPierre-Marie Pédrot
2018-12-18Merge PR #9178: CoqIDE: Restoring configuration of default width/height of ↵Pierre-Marie Pédrot
main window.
2018-12-18Merge PR #9215: Set up CI with Azure PipelinesEmilio Jesus Gallego Arias
2018-12-17Merge PR #9153: [api] Move reduction modules to `tactics`Pierre-Marie Pédrot
2018-12-17[STM] Better protection for cur_idMaxime 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-17Merge PR #9238: CI: simple-io now depends on ext-libEmilio Jesus Gallego Arias
2018-12-17Set up CI with Azure PipelinesGaëtan Gilbert
2018-12-17simple-io now depends on ext-libGaëtan Gilbert
2018-12-17Merge PR #8856: [gitlab] Test Ocaml trunk.Gaëtan Gilbert
2018-12-17Fix git line ending conversion in windowsGaëtan Gilbert
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-12-17Merge PR #9206: [stm] join the tip of the document even when fixing a proof ↵Emilio Jesus Gallego Arias
(fix #9204)
2018-12-17Merge PR #9219: [STM] Fix logic of debug DAG printerEnrico Tassi
2018-12-17Merge PR #9220: Move shallow state logic to the function preparing state for ↵Enrico Tassi
workers
2018-12-17CoqIDE: 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-16Merge PR #9172: [proof] Rework proof interface.Pierre-Marie Pédrot
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-14Merge PR #9073: [sphinx] No more undocumented objects.Clément Pit-Claudel
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-14Merge 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-14Update pinned nixpkgs to use Dune 1.6.Théo Zimmermann
2018-12-14Turn warning on for undocumented objects. Closes #7602.Théo Zimmermann
2018-12-14Fix the SSReflect chapter regarding objects without bodies.Théo Zimmermann
2018-12-14Do not raise object without body warning for prodn objects.Théo Zimmermann
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost ↵Gaëtan Gilbert
of evars in shelf)
2018-12-13Merge PR #9194: Fixing uses of sed in #8985 which do not work on MacOS XMatthieu Sozeau
2018-12-13Fixing uses of sed which do not work on MacOS X.Hugo Herbelin
This was introduced in PR #8985.
2018-12-13Merge PR #9117: Accept argument names for extra arguments with "extra scopes"Matthieu Sozeau
2018-12-13Add overlayMaxime Dénès
2018-12-13Merge PR #9210: Fix issue #9176 : Windows: change cygwin repoThéo Zimmermann
2018-12-13Merge 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-13Merge PR #9032: checker: check inductive types by roundtrip through the kernel.Pierre-Marie Pédrot
2018-12-13Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as ↵Pierre-Marie Pédrot
pattern variables
2018-12-13Merge PR #9169: [rtauto] [auto] Use new proof engine.Pierre-Marie Pédrot
2018-12-13Merge 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 offEnrico Tassi
2018-12-13[stm] join: check no error states are part of the documentEnrico Tassi
The error-resiliency feature may have managed to reach the end of the document by recovering some error
2018-12-13Merge PR #9196: Document the deprecation of hint declaration withou database ↵Maxime Dénès
in refman.
2018-12-13[test] for #9204Enrico Tassi
2018-12-13[stm] join the tip of the document even when fixing a proof (fix #9204)Enrico Tassi
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-12-13[STM] Fix logic of debug DAG printerMaxime Dénès
2018-12-13Merge PR #8096: Higher-level libobject API for objects with fixed scopesEnrico Tassi
2018-12-13[ci] [appveyor] Temporally disable test suite on Appveyor.Emilio Jesus Gallego Arias
Hopefully we will re-enable it back soon, I am preparing a refactoring that should make it more robust w.r.t paths and changes on Windows which will enable to use a faster build system. But now it is timing out 100% of the times [due to #8655] so it is not useful.
2018-12-12Merge PR #9101: Fix 8922 againHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-12 07:30:13 +0000