Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / LPCIC/coq-elpi issues and pull requests

#91 - [coq] Adapt to coq/coq#9867

Pull Request - State: closed - Opened by proux01 over 5 years ago - 2 comments

#90 - Adapt to coq/coq#11027 (inductive entries use boolean for cumulativity)

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

#89 - [coq] Adapt to coq/coq#10516

Pull Request - State: closed - Opened by ejgallego over 5 years ago - 1 comment

#88 - coq-elaborator and no-ops

Issue - State: closed - Opened by gares over 5 years ago

#87 - antiquotation in binder scope

Issue - State: open - Opened by gares over 5 years ago - 1 comment

#86 - coq.env.typeof-gr -> coq.env.typeof

Issue - State: closed - Opened by gares over 5 years ago

#85 - Adapt to coq/coq#10786 (Attempt to allow coercions between SProp and sorts)

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

#84 - Param2 const type

Pull Request - State: closed - Opened by CohenCyril over 5 years ago - 1 comment

#83 - Adapt to coq/coq#10811 (SProp default on)

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

#82 - Readd dune

Pull Request - State: closed - Opened by ejgallego over 5 years ago - 23 comments

#81 - examples

Issue - State: closed - Opened by gares over 5 years ago - 1 comment

#80 - [derive] provide a link to mathcomp

Issue - State: open - Opened by gares over 5 years ago

#79 - sync with master + elpi1.7

Pull Request - State: closed - Opened by gares over 5 years ago - 2 comments

#78 - port to elpi 1.7 + rm hole term constructor

Pull Request - State: closed - Opened by gares over 5 years ago

#77 - [coq] Adapt to coq/coq#10727

Pull Request - State: closed - Opened by ejgallego over 5 years ago - 1 comment

#76 - [coq] Adapt to coq/coq#10665

Pull Request - State: closed - Opened by ejgallego over 5 years ago - 1 comment

#75 - Adapt to coq/coq#10642 (feedback AddedAxiom at the Declare layer)

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

#74 - Tutorial typos

Pull Request - State: closed - Opened by robblanco over 5 years ago - 1 comment

#73 - Overlay rm library optim

Pull Request - State: closed - Opened by gares over 5 years ago - 6 comments

#72 - jscoq tutorials

Issue - State: closed - Opened by gares over 5 years ago - 2 comments

#71 - put back string quotations for legacy ui

Issue - State: closed - Opened by gares over 5 years ago - 1 comment

#70 - remove hole

Issue - State: closed - Opened by gares over 5 years ago - 1 comment

#69 - [coq] Overlay for coq/coq#10419

Pull Request - State: closed - Opened by ejgallego over 5 years ago - 1 comment

#68 - Adapt to coq/coq#10390 (UIP in SProp)

Pull Request - State: closed - Opened by SkySkimmer over 5 years ago

#67 - adapt to coq/coq#10416

Pull Request - State: closed - Opened by gares over 5 years ago - 3 comments

#66 - [coq] Overlay for coq/coq#10316

Pull Request - State: closed - Opened by ejgallego over 5 years ago - 1 comment

#65 - Fix w.r.t. coq/coq#10362.

Pull Request - State: closed - Opened by ppedrot over 5 years ago - 1 comment

#64 - overlay for coq#10358

Pull Request - State: closed - Opened by gares over 5 years ago - 1 comment

#63 - Adapt to Coq PR #8988: change of type internal syntax

Pull Request - State: closed - Opened by herbelin over 5 years ago - 3 comments

#62 - Adapting to Coq PR #8726

Pull Request - State: closed - Opened by herbelin over 5 years ago - 2 comments

#61 - Fix for coq/coq#10201.

Pull Request - State: closed - Opened by ppedrot over 5 years ago - 1 comment

#59 - Adapt to coq/coq#10157 (Higher level implementation of definition-not-visible warning)

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

#58 - [coq] Adapt to coq/coq#9867

Pull Request - State: closed - Opened by proux01 over 5 years ago - 3 comments

#57 - Fix for Coq PR#10076

Pull Request - State: closed - Opened by vbgl over 5 years ago

#56 - Adapt to coq/coq#10050 (proof_global API changes)

Pull Request - State: closed - Opened by SkySkimmer almost 6 years ago - 1 comment

#55 - [coq] Fix warning about unused open.

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 3 comments

#54 - Elpi1.2

Pull Request - State: closed - Opened by gares almost 6 years ago - 1 comment

#53 - [coq] Adapt to coq/coq#9165

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 4 comments

#52 - Adapt to Coq's PR #9909

Pull Request - State: closed - Opened by maximedenes almost 6 years ago - 1 comment

#51 - Fix for Coq PR#9870

Pull Request - State: closed - Opened by vbgl almost 6 years ago

#50 - [coq] Overlay for coq/coq#9566

Pull Request - State: closed - Opened by ejgallego almost 6 years ago - 1 comment

#49 - Adapt to changes in Coq's printers API

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

#48 - [coq] Adapt to coq/coq#9129 "removal of imperative proof state"

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

#47 - Fix warnings regarding primitive integers

Pull Request - State: closed - Opened by vbgl almost 6 years ago - 1 comment

#46 - Adapt to coq/coq#9439 (separate variance and universes in inductives)

Pull Request - State: closed - Opened by SkySkimmer almost 6 years ago - 1 comment

#45 - Adapt to coq/coq#8817 (SProp)

Pull Request - State: closed - Opened by SkySkimmer about 6 years ago - 6 comments

#44 - [coq overlay] Adapt to coq/coq#9102

Pull Request - State: closed - Opened by ejgallego about 6 years ago - 1 comment

#43 - [coq overlay] Adapt to coq/coq#8705

Pull Request - State: closed - Opened by ejgallego about 6 years ago - 1 comment

#42 - [coq] Adapt to coq/coq#9065

Pull Request - State: closed - Opened by ejgallego about 6 years ago - 1 comment

#41 - [coq] Adapt to packing of gramlib Coq coq/coq#8985

Pull Request - State: closed - Opened by ejgallego about 6 years ago - 2 comments

#40 - Port to coqpp

Pull Request - State: closed - Opened by ppedrot over 6 years ago

#39 - Adapt to coq/coq#8718: change of API around declaration hooks

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

#38 - Adapt to API after coq#8684

Pull Request - State: closed - Opened by maximedenes over 6 years ago - 1 comment

#37 - Adapt to API after coq#8684

Pull Request - State: closed - Opened by maximedenes over 6 years ago

#36 - Overlay for Coq #8688 (evar printers generalized over env)

Pull Request - State: closed - Opened by herbelin over 6 years ago - 3 comments

#35 - [Makefile] COQBIN needs a trailing separator “/”

Pull Request - State: closed - Opened by vbgl over 6 years ago - 1 comment

#34 - Adapt to Coq's PR 8704

Pull Request - State: closed - Opened by ejgallego over 6 years ago - 2 comments

#33 - [coq] Fix Ltac qualification.

Pull Request - State: closed - Opened by ejgallego over 6 years ago - 1 comment

#32 - Overlay/8456

Pull Request - State: closed - Opened by gares over 6 years ago

#31 - Fix compilation for coq/coq#8601.

Pull Request - State: closed - Opened by ppedrot over 6 years ago - 1 comment

#30 - [api] [coq] Don't use deprecated record field.

Pull Request - State: closed - Opened by ejgallego over 6 years ago - 2 comments

#29 - [Coq 8.9+] Please fix deprecation warnings

Issue - State: closed - Opened by ejgallego over 6 years ago - 6 comments

#28 - Fix for coq/coq#7906 (universes_of_constr doesn't need an env)

Pull Request - State: closed - Opened by SkySkimmer over 6 years ago - 3 comments

#27 - Fix for coq/coq#7863 (removed Sorts.contents)

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

#26 - Misc fixes

Pull Request - State: closed - Opened by SkySkimmer over 6 years ago - 3 comments

#25 - use @pi-decl and @pi-def everywhere

Issue - State: closed - Opened by gares over 6 years ago

#24 - Adapt to Coq's PR #7797 (removal of reference).

Pull Request - State: closed - Opened by maximedenes over 6 years ago

#23 - Document how to compile against a local Coq version

Issue - State: closed - Opened by maximedenes over 6 years ago - 1 comment

#22 - derive is incomplete (does not call eqOK)

Issue - State: closed - Opened by gares over 6 years ago

#21 - HOAS of context is incomplete (if not decl/def then assert false)

Issue - State: closed - Opened by gares over 6 years ago - 1 comment

#20 - document CIC coverage of each derivation

Issue - State: closed - Opened by gares over 6 years ago - 1 comment

#19 - whd1 in all derivations

Issue - State: closed - Opened by gares over 6 years ago - 1 comment

#18 - Adapting to Coq PR #7080: Named.Context.t -> Constr.named_context.

Pull Request - State: closed - Opened by herbelin almost 7 years ago - 1 comment

#17 - Adapt to coq/coq#7136 (econstr in Evd)

Pull Request - State: closed - Opened by SkySkimmer almost 7 years ago - 4 comments

#16 - [coq] Adapt to coq/coq#7152.

Pull Request - State: closed - Opened by ejgallego almost 7 years ago - 3 comments

#15 - whd1 in all API/coq-lib

Issue - State: open - Opened by gares almost 7 years ago - 1 comment

#14 - Remove/GProj

Pull Request - State: closed - Opened by gares almost 7 years ago - 6 comments

#13 - Adapt to coq/coq#6775 (weak constraints for cumulative inductives).

Pull Request - State: closed - Opened by SkySkimmer almost 7 years ago - 2 comments

#12 - [coq] Adapt to coq/coq#6837.

Pull Request - State: closed - Opened by ejgallego almost 7 years ago - 2 comments

#11 - [coq] Adapt to coq/coq#6831.

Pull Request - State: closed - Opened by ejgallego almost 7 years ago - 1 comment

#10 - [coq] Adapt to coq/coq#6745

Pull Request - State: closed - Opened by ejgallego almost 7 years ago - 2 comments

#9 - ltac.elpi

Issue - State: open - Opened by gares about 7 years ago

#8 - collect-goals

Issue - State: closed - Opened by gares about 7 years ago

#7 - Broken in 4.06.0 [-safe-string]

Issue - State: closed - Opened by ejgallego about 7 years ago - 2 comments

#6 - Port param to the new API for databases

Issue - State: closed - Opened by gares about 7 years ago - 3 comments
Labels: enhancement

#5 - full round trip for Coq's engine

Pull Request - State: closed - Opened by gares about 7 years ago

#4 - Redesign/hochr

Pull Request - State: closed - Opened by gares about 7 years ago

#2 - Search elpi files in $COQPATH

Pull Request - State: closed - Opened by vbgl over 7 years ago - 1 comment

#1 - Clean up ctypes for names

Issue - State: closed - Opened by gares over 7 years ago
Labels: enhancement