aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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.
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.
2018-11-16Merge PR #8779: Remove the implicit tactic feature following #7229.Matthieu Sozeau
2018-11-16Merge PR #8781: Remove primproj <-> constant dependency in HeadsPierre-Marie Pédrot
2018-11-16Reimplement Store using Dyn.whitequark
2018-11-16Add Dyn.anonymous, a more efficient version of Dyn.create (string_of_int n).whitequark
2018-11-16Use universe names when printing to dot.Gaëtan Gilbert
2018-11-16Print Universes SubgraphGaëtan Gilbert
This adds an optional [Subgraph] part to the Print Universes command, eg [Print Universes Subgraph(i j)] to print only constraints related to i and j (and Prop/Set).
2018-11-16Make UGraph printing independent of hash orderGaëtan Gilbert
2018-11-16Print universe names in subtyping error instead of Var(x).Gaëtan Gilbert
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
Use of boxes to ensure locality of formatting + use of a prlist_with_sep so that there are breaking points only inbetween the elements and not at the end of the list.
2018-11-16Print full binders in subtyping incompatible polymorphism error.Gaëtan Gilbert
Close #8891
2018-11-16put protocol/ in ide/.merlinGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:57:17 +0000