ejgallego/coq-serapi issues and pull requests

#426 - Adapt to https://github.com/coq/coq/pull/19370

Pull Request - State: open - Opened by proux01 about 1 month ago

#425 - Adapt to https://github.com/coq/coq/pull/19530

Pull Request - State: open - Opened by proux01 about 2 months ago

#424 - Adapt w.r.t. coq/coq#19481.

Pull Request - State: closed - Opened by ppedrot 3 months ago
Labels: kind: upstream

#423 - [ci] Build Coq after final OPAM setup.

Pull Request - State: closed - Opened by ejgallego 3 months ago
Labels: kind: infrastructure

#422 - Adapt to https://github.com/coq/coq/pull/19310

Pull Request - State: closed - Opened by proux01 4 months ago - 1 comment
Labels: kind: upstream

#421 - adapt to coq/coq#19147

Pull Request - State: closed - Opened by gares 5 months ago

#420 - [PATCH] Compilation with yojson >= 2.2

Issue - State: closed - Opened by SnarkBoojum 5 months ago - 4 comments
Labels: kind: bug, sexplib

#419 - [coq] Adapt to coq/coq#19193

Pull Request - State: closed - Opened by ejgallego 5 months ago
Labels: kind: upstream

#418 - CoqSerapi Usage Question

Issue - State: closed - Opened by ana-brendel 5 months ago - 6 comments
Labels: question

#417 - [coq] Adapt to coq/coq#19187

Pull Request - State: closed - Opened by ejgallego 5 months ago
Labels: kind: upstream

#416 - Adapt to coq/coq#18973.

Pull Request - State: closed - Opened by rlepigre 5 months ago - 1 comment
Labels: kind: upstream

#415 - [serlib] Don't use compat type Result.result

Pull Request - State: closed - Opened by ejgallego 6 months ago
Labels: kind: bug, kind: infrastructure

#414 - [serlib] [ltac2] Test for Ltac2 serialization

Pull Request - State: open - Opened by ejgallego 6 months ago
Labels: kind: serialization

#413 - [serlib] [ltac2] Fix wrong piercing creating havoc.

Pull Request - State: closed - Opened by ejgallego 6 months ago
Labels: kind: bug, kind: upstream, kind: serialization

#412 - Adapt to coq/coq#19078 (different module type for unordered maps)

Pull Request - State: closed - Opened by SkySkimmer 6 months ago - 1 comment
Labels: kind: upstream

#411 - License issue

Issue - State: closed - Opened by SnarkBoojum 6 months ago - 1 comment

#410 - [opam] Allow Coq dev version on constraint.

Pull Request - State: closed - Opened by ejgallego 6 months ago
Labels: kind: infrastructure

#409 - [serlib] Remove serlib and use coq-lsp serlib version instead.

Pull Request - State: closed - Opened by ejgallego 6 months ago
Labels: kind: infrastructure, kind: meta, kind: cleanup, fixed by: flèche

#408 - [coq] Overlay for coq/coq#18385

Pull Request - State: closed - Opened by ejgallego 6 months ago - 1 comment
Labels: kind: upstream

#407 - [ci] Rework CI as to be more modular

Pull Request - State: closed - Opened by ejgallego 7 months ago
Labels: kind: testing, kind: infrastructure, kind: meta

#406 - Backports for 8.19.3

Pull Request - State: closed - Opened by ejgallego 7 months ago
Labels: kind: meta

#405 - Adapt to coq/coq#18938 (EConstr.ERelevance)

Pull Request - State: closed - Opened by SkySkimmer 7 months ago
Labels: kind: upstream

#404 - Adapt to coq/coq#18771 (Improve handling of Drop)

Pull Request - State: closed - Opened by afdw 7 months ago
Labels: kind: upstream

#403 - [upstream] Fix breaking merge in Coq upstream.

Pull Request - State: closed - Opened by ejgallego 7 months ago
Labels: kind: upstream

#402 - Adapt to coq/coq#18852 (interp_red_expr can be done without ltac)

Pull Request - State: closed - Opened by SkySkimmer 8 months ago
Labels: kind: upstream

#401 - Adapt to coq/coq#18422 (indirect accessor handled through vernactypes)

Pull Request - State: closed - Opened by SkySkimmer 8 months ago
Labels: kind: upstream

#400 - New versioning scheme.

Issue - State: closed - Opened by ejgallego 8 months ago - 1 comment

#399 - [test] Don't require math-comp to run the test suite.

Pull Request - State: closed - Opened by ejgallego 8 months ago
Labels: kind: bug, kind: testing, kind: infrastructure

#398 - [serlib] Fix TODO / bug in primitive code.

Pull Request - State: closed - Opened by ejgallego 8 months ago
Labels: kind: bug, kind: serialization

#397 - Segmentation fault in coq/getDocument call

Issue - State: closed - Opened by Nfsaavedra 8 months ago - 4 comments
Labels: kind: bug, kind: upstream, kind: serialization

#396 - Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

Issue - State: closed - Opened by rtetley 8 months ago - 5 comments
Labels: question, kind: meta

#395 - Run tests with MC 2

Issue - State: closed - Opened by SnarkBoojum 8 months ago - 3 comments

#394 - Adapt to coq/coq#18719 (stricter type for vernac_argument extend)

Pull Request - State: closed - Opened by SkySkimmer 9 months ago
Labels: kind: upstream

#393 - Keep the Vmlibrary.t type opaque.

Pull Request - State: closed - Opened by ppedrot 9 months ago - 2 comments
Labels: kind: serialization

#392 - [backports] CI for 8.19.1

Pull Request - State: closed - Opened by ejgallego 9 months ago
Labels: kind: meta

#391 - [serlib] Support btauto Coq plugin

Pull Request - State: closed - Opened by ejgallego 9 months ago
Labels: kind: enhancement, kind: upstream, kind: serialization

#390 - Adapt w.r.t. coq/coq#18664.

Pull Request - State: closed - Opened by ppedrot 9 months ago
Labels: kind: upstream

#389 - Adapt w.r.t. coq/coq#17674.

Pull Request - State: closed - Opened by ppedrot 9 months ago
Labels: kind: upstream

#388 - Adapt to coq/coq#18546.

Pull Request - State: closed - Opened by rlepigre 9 months ago
Labels: kind: upstream

#387 - Adapt to coq/coq#18038 (rewrite rules)

Pull Request - State: closed - Opened by yannl35133 9 months ago - 1 comment
Labels: kind: upstream

#386 - [serlib] Expose some more functions related to Require's AST.

Pull Request - State: closed - Opened by ejgallego 9 months ago

#385 - Adapt to coq/coq#18528 (profile_ltac moved to engine and renamed profile_tactic)

Pull Request - State: closed - Opened by SkySkimmer 10 months ago
Labels: kind: upstream

#384 - [ci] Remove obsolete pin on dune for Coq git build

Pull Request - State: closed - Opened by ejgallego 10 months ago
Labels: kind: bug, kind: infrastructure

#383 - [serlib] Expose some more functions related to Require's AST.

Pull Request - State: closed - Opened by ejgallego 10 months ago
Labels: kind: enhancement, kind: serialization

#382 - macOS: serapi loads Coq .vo from compile time path

Issue - State: closed - Opened by MSoegtropIMC 10 months ago - 5 comments

#381 - Adapt to coq/coq#18352 (ltacX_common_plugin)

Pull Request - State: closed - Opened by SkySkimmer 10 months ago - 1 comment

#380 - Adapt to coq/coq#18094: rewrite strategies: fix

Pull Request - State: closed - Opened by JasonGross 11 months ago - 2 comments
Labels: kind: upstream

#379 - Adapt to #18229: nested_type is now recarg_type (no more "nested" mark)

Pull Request - State: closed - Opened by herbelin 11 months ago
Labels: kind: upstream

#378 - Adapt to coq/coq#18143 (debug printing for relevances)

Pull Request - State: closed - Opened by SkySkimmer 11 months ago
Labels: kind: upstream

#377 - Windows PATH length (again)

Issue - State: closed - Opened by MSoegtropIMC 11 months ago - 21 comments

#376 - Adapt to coq/coq#18327 (projection opacity)

Pull Request - State: closed - Opened by rlepigre 11 months ago
Labels: kind: upstream

#375 - Support the extraction plugin

Pull Request - State: closed - Opened by toku-sa-n 12 months ago - 2 comments
Labels: kind: enhancement, kind: upstream, kind: serialization

#374 - Adapt to coq/coq#18331 (sort poly inductives)

Pull Request - State: closed - Opened by SkySkimmer 12 months ago
Labels: kind: upstream

#373 - Can't run `make test` due to an error related to `eqType`

Issue - State: closed - Opened by toku-sa-n 12 months ago - 4 comments

#372 - Adapt w.r.t. coq/coq#18345.

Pull Request - State: closed - Opened by ppedrot 12 months ago
Labels: kind: upstream

#371 - Missing conversion functions for types for the extraction plugin?

Issue - State: closed - Opened by toku-sa-n 12 months ago - 3 comments

#370 - Adapt w.r.t. coq/coq#18312.

Pull Request - State: closed - Opened by ppedrot 12 months ago
Labels: kind: upstream

#369 - Adapt w.r.t. coq/coq#18294.

Pull Request - State: closed - Opened by ppedrot about 1 year ago
Labels: kind: upstream

#368 - Adapt to coq/coq#18280 (case relevance outside case info)

Pull Request - State: closed - Opened by SkySkimmer about 1 year ago
Labels: kind: upstream

#366 - Adapt to https://github.com/coq/coq/pull/14928

Pull Request - State: closed - Opened by proux01 about 1 year ago - 1 comment

#365 - remove all references to deprecated Arith modules from genarg tests

Pull Request - State: closed - Opened by palmskog about 1 year ago - 1 comment
Labels: kind: upstream, kind: testing

#364 - Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

Issue - State: closed - Opened by rtetley about 1 year ago - 1 comment

#363 - Adapt w.r.t coq/coq#18124 (Remove the TacComplete AST)

Pull Request - State: closed - Opened by LasseBlaauwbroek about 1 year ago
Labels: kind: upstream

#362 - [general] Cleanup old unused code.

Pull Request - State: closed - Opened by ejgallego about 1 year ago
Labels: kind: cleanup

#361 - [doc] [license] Improve licensing situation.

Pull Request - State: closed - Opened by ejgallego about 1 year ago - 1 comment
Labels: kind: documentation, kind: meta

#360 - Adapt to coq/coq#17503 (raw/glob_red_expr moved)

Pull Request - State: closed - Opened by SkySkimmer about 1 year ago - 2 comments
Labels: kind: upstream

#359 - Adapt to coq/coq#17667 (handle genarg in patterns)

Pull Request - State: closed - Opened by SkySkimmer about 1 year ago
Labels: kind: upstream

#358 - Adapt to coq/coq#17836 (sort poly)

Pull Request - State: closed - Opened by SkySkimmer about 1 year ago
Labels: kind: upstream

#357 - [serlib] Fix some 8.18 piercings

Pull Request - State: closed - Opened by ejgallego about 1 year ago
Labels: kind: bug, kind: upstream, kind: serialization

#356 - [serlib] [doc] Add some readme with serlib documentation.

Pull Request - State: closed - Opened by ejgallego about 1 year ago - 3 comments
Labels: kind: documentation

#355 - Adapt to coq/coq#18010 (monomorphized vernac_expr)

Pull Request - State: closed - Opened by SkySkimmer about 1 year ago

#354 - Adapt to Coq PR #17987 which adds sigma to the API of search functions

Pull Request - State: closed - Opened by herbelin about 1 year ago
Labels: kind: upstream

#353 - Adapt to coq/coq#17928 (Search uses search_restriction instead of bool)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago
Labels: kind: upstream

#352 - Adapt to https://github.com/coq/coq/pull/17875

Pull Request - State: closed - Opened by proux01 over 1 year ago - 1 comment
Labels: kind: upstream

#351 - [serlib] Compat with JS libs >= v0.16.0

Pull Request - State: closed - Opened by ejgallego over 1 year ago
Labels: kind: enhancement

#350 - [ci] Update action/checkout to @v3

Pull Request - State: closed - Opened by ejgallego over 1 year ago

#349 - [serlib] Fix ltac2 plugin wrong piercing

Pull Request - State: closed - Opened by ejgallego over 1 year ago
Labels: kind: bug, kind: upstream, kind: serialization

#348 - Incorrect goals when providing -topfile in sertop 8.10.0+0.7.2

Issue - State: closed - Opened by a-gardner1 over 1 year ago - 2 comments

#347 - Adapt to #17827: new type Notation_term.notation_var_binders

Pull Request - State: closed - Opened by herbelin over 1 year ago - 3 comments
Labels: kind: upstream

#346 - Adapt to coq/coq#17795 (UState.rigid used in glob_term)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago
Labels: kind: upstream

#345 - Adapt to coq/coq#17754

Pull Request - State: closed - Opened by proux01 over 1 year ago
Labels: kind: upstream

#344 - Adapt w.r.t. coq/coq#17719.

Pull Request - State: closed - Opened by ppedrot over 1 year ago - 2 comments
Labels: kind: upstream

#343 - [build] Rectypes are not needed in Coq anymore.

Pull Request - State: closed - Opened by ejgallego over 1 year ago
Labels: kind: upstream, kind: infrastructure

#342 - [serapi] New protocol call `SecVars`

Pull Request - State: closed - Opened by ejgallego over 1 year ago - 3 comments
Labels: kind: enhancement, protocol

#341 - [ci] Fix 32bit gcc setup failure.

Pull Request - State: closed - Opened by ejgallego over 1 year ago
Labels: kind: bug, kind: infrastructure

#340 - [sertop] [coq] Don't initialize CoqworkmgrApi

Pull Request - State: closed - Opened by ejgallego over 1 year ago
Labels: kind: upstream, kind: cleanup

#339 - Expose Section Variable Determining API in SerAPI

Issue - State: closed - Opened by HazardousPeach over 1 year ago - 6 comments
Labels: kind: enhancement, protocol, kind: upstream

#338 - Adapt to coq/coq#17699 (pcant_apply_bad_type)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago
Labels: kind: upstream

#337 - Adapt to coq/coq#17359 (ltac2_var_quotation)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago
Labels: kind: upstream

#336 - Adapt to coq/coq#17696 (Mltop.load_module is exposed)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 3 comments
Labels: kind: upstream

#335 - Adapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago - 1 comment

#334 - Adapt to coq/coq#17662 (qvar representation changed)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago

#333 - Adapt to coq/coq#17575 (ltac2val in ltac1)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago

#332 - What is the purpose of coq-serapi's existance and why can't everything be done in coqtop?

Issue - State: closed - Opened by brando90 over 1 year ago - 5 comments
Labels: question

#331 - Segfault on (Query () Goals) with sertop 8.15.0+0.15.3

Issue - State: closed - Opened by rwhender over 1 year ago - 4 comments

#330 - Adapt to coq/coq#17505 (UGraph.explanation changed)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago
Labels: kind: upstream

#323 - Adapt to coq/coq#17293 (wit_red_expr moved)

Pull Request - State: closed - Opened by SkySkimmer over 1 year ago

#313 - Adapt to #17117: level is now in notationterm.ml, side in constrexpr.ml

Pull Request - State: closed - Opened by herbelin almost 2 years ago - 6 comments

#266 - Licensing needs to be clarified

Issue - State: closed - Opened by SnarkBoojum over 2 years ago - 18 comments

#227 - Support for 8.13?

Issue - State: closed - Opened by gmalecha almost 4 years ago - 4 comments

GitHub / ejgallego/coq-serapi issues and pull requests