Ecosyste.ms: Issues

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

GitHub / Mtac2/Mtac2 issues and pull requests

#386 - Turn `unify_univ` into `unify_cumul_cnt`.

Pull Request - State: closed - Opened by Janno over 1 year ago - 2 comments

#385 - Check the result of `M.hyps` against the expected universes

Pull Request - State: closed - Opened by Janno over 1 year ago - 2 comments

#384 - Fixing unsoundness in abs_prod_type (master)

Pull Request - State: closed - Opened by Janno over 1 year ago - 3 comments

#383 - Less specific pattern type & better mmatch syntax & more (redux)

Pull Request - State: closed - Opened by Janno over 1 year ago - 4 comments

#382 - Print type error instead of `"different type"`

Issue - State: open - Opened by Janno over 1 year ago

#381 - Fixing unsoundness in abs_prod_type

Pull Request - State: open - Opened by beta-ziliani over 1 year ago

#380 - `decompose_app'` should just unify the two terms

Issue - State: open - Opened by Janno over 1 year ago

#379 - Adapt to coq/coq#16890 (Classes.existing_instance takes GlobRef not qualid)

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

#378 - Adapt to coq/coq#17453 (Reduction->Conversion)

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

#377 - Please create a tag for Coq 8.17 in Coq Platform 2023.03

Issue - State: closed - Opened by MSoegtropIMC over 1 year ago - 3 comments

#376 - Adapt w.r.t. coq/coq#17194.

Pull Request - State: closed - Opened by ppedrot over 1 year ago - 4 comments

#375 - metaCoqInit: replace Pcoq.Entry.create with Pcoq.Entry.make

Pull Request - State: closed - Opened by artagnon over 1 year ago - 2 comments

#374 - Do not rely on CClosure.unfold_reference.

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

#373 - Adapt w.r.t. coq/coq#17053.

Pull Request - State: closed - Opened by ppedrot over 1 year ago - 6 comments

#372 - Overlay for Coq #16981 Give an error for a non-existent proof mode in the Proof Mode command

Pull Request - State: closed - Opened by jfehrle almost 2 years ago - 5 comments

#371 - Don't force references at linking time

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

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

Pull Request - State: closed - Opened by ppedrot almost 2 years ago - 9 comments

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

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

#368 - Adapt w.r.t. coq/coq#16442.

Pull Request - State: closed - Opened by ppedrot about 2 years ago - 4 comments

#367 - Adapt w.r.t. coq/coq#16488.

Pull Request - State: closed - Opened by ppedrot about 2 years ago - 10 comments

#366 - Attempt to get bors running again.

Pull Request - State: closed - Opened by Janno about 2 years ago - 4 comments

#365 - Address most build warnings and fix a typo

Pull Request - State: closed - Opened by Janno about 2 years ago

#364 - CI for 8.16

Pull Request - State: closed - Opened by beta-ziliani about 2 years ago - 3 comments

#363 - Please create a tag for Coq 8.16 in Coq Platform 2022.09

Issue - State: closed - Opened by MSoegtropIMC about 2 years ago - 4 comments

#362 - adapt to coq/coq#16361

Pull Request - State: open - Opened by gares about 2 years ago

#361 - improved auto goal selection

Pull Request - State: closed - Opened by mrhaandi about 2 years ago

#360 - Stop using deprecated Globnames APIs

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

#359 - Adapt w.r.t coq/coq#16004

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

#358 - Debug CI problems

Pull Request - State: closed - Opened by Janno over 2 years ago - 4 comments

#357 - Adapt w.r.t. coq/coq#15871.

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

#356 - Adapt to coq/coq#15693

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

#355 - Adapt to coq/coq#15853

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

#354 - Adapt to coq/coq#15807 (delayed univ subst in cclosure)

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

#353 - Disable Universe Minimization ToSet in DepDestruct tests.

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

#352 - Adapt w.r.t. coq/coq#15837.

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

#351 - Adapt to Coq PR #15537: schemes mrec_rect & cie have different automatically generated names

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

#350 - Please create a tag for Coq 8.15 in Coq Platform 2022.02

Issue - State: closed - Opened by MSoegtropIMC over 2 years ago - 4 comments

#349 - adapt to coq/coq#15220

Pull Request - State: closed - Opened by gares almost 3 years ago - 4 comments

#348 - Adapt w.r.t. coq/coq#15119.

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

#347 - Adapt w.r.t. coq/coq#15069.

Pull Request - State: closed - Opened by ppedrot almost 3 years ago - 11 comments

#346 - Adapt to coq/coq#15003 (user_err has no hdr argument)

Pull Request - State: closed - Opened by SkySkimmer almost 3 years ago - 9 comments

#345 - Create master-8.14 branch

Pull Request - State: closed - Opened by Janno about 3 years ago - 3 comments

#344 - Please create a tag for the upcoming release of Coq 8.14

Issue - State: closed - Opened by MSoegtropIMC about 3 years ago - 2 comments

#343 - Adapt w.r.t. coq/coq#14903.

Pull Request - State: closed - Opened by ppedrot about 3 years ago - 11 comments

#342 - Adapting to Coq PR #14711: Evd.univ_entry returns also the universe binders

Pull Request - State: closed - Opened by herbelin about 3 years ago - 9 comments

#341 - Fixes for coq#14808

Pull Request - State: closed - Opened by Janno about 3 years ago - 2 comments

#340 - Adapt to coq/coq#14819

Pull Request - State: closed - Opened by proux01 about 3 years ago - 2 comments

#339 - Adapt w.r.t. coq/coq#14810.

Pull Request - State: closed - Opened by ppedrot about 3 years ago - 10 comments

#337 - Adapt to coq/coq#14646 (removal of safe_evar_value alias)

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

#336 - [coq] Fix use of deprecated function

Pull Request - State: closed - Opened by ejgallego over 3 years ago - 4 comments

#335 - Overlay for Coq PR 14224

Pull Request - State: closed - Opened by jfehrle over 3 years ago - 8 comments

#334 - Less specific pattern type & better mmatch syntax & more

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

#333 - [8.13] Fix LHS & RHS of cumul. unif in mrun typecheck

Pull Request - State: closed - Opened by Janno over 3 years ago - 1 comment

#332 - [8.13] Move CI to Github Actions

Pull Request - State: closed - Opened by Janno over 3 years ago - 2 comments

#331 - Use non-delaying variant of `unify` in `ifM`

Issue - State: open - Opened by Janno over 3 years ago

#330 - Adapt w.r.t coq/coq#14148.

Pull Request - State: closed - Opened by ppedrot over 3 years ago - 14 comments

#329 - WIP: Move CI to GitHub Actions

Pull Request - State: closed - Opened by Janno over 3 years ago - 13 comments
Labels: backport master-8.13

#328 - Fix LHS & RHS of cumul. unif in `mrun` typecheck

Pull Request - State: closed - Opened by Janno over 3 years ago - 6 comments
Labels: backport master-8.13

#326 - Lazily update universes in sigma

Issue - State: open - Opened by Janno over 3 years ago - 3 comments

#325 - Possible performance improvements

Issue - State: open - Opened by Janno over 3 years ago
Labels: enhancement

#324 - adapt to coq/coq#13958

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

#323 - removing omega

Pull Request - State: closed - Opened by beta-ziliani over 3 years ago - 2 comments

#322 - Adapt w.r.t. coq/coq#13563

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

#321 - Backporting 8.12

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

#320 - Various performance improvements

Pull Request - State: closed - Opened by Janno almost 4 years ago - 5 comments

#319 - [8.12] Various performance improvements

Pull Request - State: closed - Opened by Janno almost 4 years ago - 2 comments

#318 - Make names of operations uniform

Issue - State: open - Opened by beta-ziliani almost 4 years ago

#317 - Remove all references to MetaCoq

Issue - State: open - Opened by beta-ziliani almost 4 years ago

#314 - Remove `read_line`

Issue - State: open - Opened by beta-ziliani almost 4 years ago

#313 - Upstream recent improvements

Pull Request - State: closed - Opened by Janno almost 4 years ago - 3 comments

#312 - Adapt w.r.t. coq/coq#13537.

Pull Request - State: closed - Opened by ppedrot almost 4 years ago - 3 comments

#311 - [8.12] Upstream recent improvements

Pull Request - State: closed - Opened by Janno almost 4 years ago - 12 comments

#310 - Please create a tag for the upcoming release of Coq 8.13

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

#309 - Compatibility for coq/coq#12449 (Minimize Prop <= i to i := Set)

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

#308 - adapt to coq/coq#13088

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

#307 - updated test case

Pull Request - State: closed - Opened by beta-ziliani about 4 years ago - 10 comments

#306 - Check result of `run` against expected type

Issue - State: open - Opened by Janno about 4 years ago

#305 - fixed #304 abs_let unsoundness

Pull Request - State: closed - Opened by beta-ziliani about 4 years ago - 4 comments

#303 - fixed #302

Pull Request - State: closed - Opened by beta-ziliani about 4 years ago - 2 comments

#301 - Fix of #299

Pull Request - State: closed - Opened by beta-ziliani about 4 years ago - 38 comments

#300 - bug uncovering an unsoundness in Mtac2

Pull Request - State: closed - Opened by beta-ziliani about 4 years ago - 4 comments

#299 - A (rather contrive) unsoundness

Issue - State: closed - Opened by beta-ziliani about 4 years ago

#293 - Tag for 8.11.2 and 8.12.0 / Opam packages / Coq platform inclusion

Issue - State: closed - Opened by MSoegtropIMC about 4 years ago - 11 comments

#292 - Universe Issue with meta-interpreters

Issue - State: open - Opened by gmalecha about 4 years ago - 11 comments

#291 - Adapt to coq/coq#12653 (syntax for cumulative inductives)

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

#283 - [8.11] Cleaning up the pattern & branch types

Pull Request - State: closed - Opened by Janno about 4 years ago - 10 comments

#278 - [coq] Adapt to coq/coq#12611

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

#276 - [8.11] Add `set_evar` primitive.

Pull Request - State: closed - Opened by Janno over 4 years ago - 1 comment

#275 - Add `set_evar` primitive.

Pull Request - State: closed - Opened by Janno over 4 years ago - 3 comments

#265 - Adapt to coq/coq#11836

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

#262 - Fix w.r.t. coq/coq#11896.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 3 comments

#261 - Fix w.r.t. coq/coq#11764.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 3 comments

#249 - Check result of `run` against expected type.

Pull Request - State: closed - Opened by Janno over 4 years ago - 1 comment

#205 - `replace` should only work if the equality proof is `meq_refl`

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