aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-21Merge PR #8961: dune: link kernel in checker instead of copying filesPierre-Marie Pédrot
2018-11-21Merge PR #8998: [legacy proof engine] Remove some cruft.Pierre-Marie Pédrot
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps.
2018-11-20Merge PR #8948: [dune] Some tweaks to docs.Théo Zimmermann
2018-11-20Merge PR #9035: [dune] Only build printers when the ltac plugin is available.Théo Zimmermann
2018-11-20[dune] Only build printers when the ltac plugin is available.Emilio Jesus Gallego Arias
This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be able to have a clean build of core Coq.
2018-11-20Merge PR #8959: [dune] [ide] Install data files.Enrico Tassi
2018-11-20Merge PR #9016: PRINT_LOGS=1 in appveyor test suite runEnrico Tassi
2018-11-20Merge PR #9017: Remove SSR profilingEnrico Tassi
2018-11-20Merge PR #9033: gitlab: Install stdlib doc in build:baseEmilio Jesus Gallego Arias
2018-11-20gitlab: Install stdlib doc in build:baseGaëtan Gilbert
Looks like we forgot to adapt this when we split off the sphinx job and stopped using -with-doc yes.
2018-11-20Merge PR #9031: Rename gh->bug_ test filesEmilio Jesus Gallego Arias
2018-11-20Merge PR #8982: [proof] Provide better control of "open proofs" exceptions.Pierre-Marie Pédrot
2018-11-20Merge PR #9002: [pfedit] Remove `start_proof` stub from `Pfedit`Pierre-Marie Pédrot
2018-11-20Rename gh->bug_ test filesGaëtan Gilbert
2018-11-20dune: link kernel in checker instead of copying filesGaëtan Gilbert
This allows to use the nice printers with constrextern etc, and since we were copying everything we're not linking any more than previously. Also the dune file is simpler without the copies.
2018-11-20Fix dune-dbg using checker/main -> checker/coqchkGaëtan Gilbert
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
2018-11-19[pfedit] Remove `start_proof` stub from `Pfedit`Emilio Jesus Gallego Arias
This way we only have 2 `start_proof` entries, in `Lemmas` and `Proof_global`; which they should be unified / brought closer in the future.
2018-11-19Merge PR #8987: Deprecate hint declaration/removal with no specified databasePierre-Marie Pédrot
2018-11-19Merge PR #9003: [vernacextend] Consolidate extension points APIPierre-Marie Pédrot
2018-11-19Merge PR #9026: [Documentation/Combined Scheme] TypoThéo Zimmermann
2018-11-19Typo: comment does not match codeOlivier Laurent
2018-11-19Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.Pierre-Marie Pédrot
2018-11-19Merge PR #8902: [ltac] Use CAst nodes in the tactic AST.Pierre-Marie Pédrot
2018-11-19Merge PR #9001: [options] Remove deprecated option automatic introduction.Pierre-Marie Pédrot
2018-11-19Merge PR #8999: [pfedit] Remove cook_proof stub.Pierre-Marie Pédrot
2018-11-19Merge PR #9023: [gramlib] Remove unused alias.Pierre-Marie Pédrot
2018-11-19Merge PR #9013: Do not Export the init modulesPierre-Marie Pédrot
2018-11-19Fix dune checker file.Pierre-Marie Pédrot
2018-11-19Adding overlays.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
This is documented in dev/doc/changes.md.
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-19Merge PR #8451: Print Universes SubgraphPierre-Marie Pédrot
2018-11-19Merge PR #7881: Reimplement Store using DynPierre-Marie Pédrot
2018-11-19[gramlib] Remove unused alias.Emilio Jesus Gallego Arias
No effect on actual code.
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
This is inspired and an alternative to #8981. We consolidate the "open proof" exception, allowing clients to explicitly capture it and removing some ugly duplicated code in the way. The `Solve Obligation tac` semantics are then tweaked as to removed the wide-scope "catch-all" and indeed will now relay errors in `tac` as it will only absorb tactics that don't error but fail to close the goal such as `auto`. For the rest of the cases, we introduce a warning, and may move to a full error in later releases. We also remove an unnecessary `tclCOMPLETE` call to code that will actually call `close_proof`. In this case, it is better to delegate error management to the core function. Some error messages have changed [as we consolidate two error paths] so this PR may require adjustment in that area.
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-18Merge PR #9018: [devtools] Small script to setup overlays automaticallyGaëtan Gilbert
2018-11-17Merge PR #8712: [stm] avoid unshare safe env to detect correctly env ↵Maxime Dénès
changing tactics
2018-11-17Merge PR #8992: put protocol/ in ide/.merlinPierre-Marie Pédrot
2018-11-17Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers.Pierre-Marie Pédrot
2018-11-17[devtools] Small script to setup overlays automaticallyEmilio Jesus Gallego Arias
This is very preliminary but you should get the idea. The script tries to build contribs, then creates a branch and sets the remote properly as to submit a PR. Usage example: ``` ./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi ``` This only works for contributions hosted in github for now.
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`.
2018-11-17[ci] Uniformize casing of makefile targets and ci variables.Emilio Jesus Gallego Arias
This is convenient as to have better automation.
2018-11-17[ci] Cleanup of old overlays.Emilio Jesus Gallego Arias
2018-11-17Merge PR #8968: Miscellaneous CoqIDE fixesPierre-Marie Pédrot
2018-11-17[pfedit] Remove cook_proof stub.Emilio Jesus Gallego Arias
This is barely used and not very useful, clients should use the close_proof API directly.
2018-11-17[CoqProject] Abstract warning function for CoqProject readers.Emilio Jesus Gallego Arias
`CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:10:42 +0000