aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-19Minor update to micromega.rstsoraros
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 remote-tracking branch 'origin/pr/84'Pierre-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-19Adding a module to manipulate Ltac1 values.Pierre-Marie Pédrot
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-19Add a function to generate fresh reference instances.Pierre-Marie Pédrot
2018-11-19Add a Char 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: Improve overlay checkGaëtan Gilbert
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-17Add an image status for the CI.Pierre-Marie Pédrot
2018-11-17Merge pull request coq/ltac2#85 from ejgallego/travisPierre-Marie Pédrot
[ci] Add travis setup, docker-based.
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[ci] Add travis setup, docker-based.Emilio Jesus Gallego Arias
Pretty straightforward; need to be enabled in the Travis console tho.
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[coq] Overlay to adapt to coq/coq#9003Emilio Jesus Gallego Arias
To be merged when the Coq developers merge the PR upstream.
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.
2018-11-17[ltac] Use CAst nodes in the tactic AST.Emilio Jesus Gallego Arias
This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 22:41:43 +0000