All pull requests

Pull requests

• improved error message for missing join

  #602·agontard opened Oct 13, 2026·

  ·
  1

• use id->name in place of string->name making the intent clear

  #597·gares opened Jun 15, 2026Member·

  ·

• solve mixin dependencies via TC

  #596·gares opened Jun 8, 2026Member·

  ·

• Interactive mode to complete instances in tactics mode

  #595·cecilemarcon opened Jun 5, 2026Collaborator·

  ·
  10

• Allow to declare instances on (fun ... => key ...)

  #594·pi8027 opened Jun 2, 2026Member·

  ·

• [freezed] reorder accumulates as allowed by Elpi 3.7

  #590·gares opened Apr 15, 2026Member·

  ·

• refactoring and correction in examples/cat.v

  #587·t6s opened Apr 1, 2026Member·

  ·
  1

  3

• Add deep-renaming elpi library

  #586·VojtechStep opened Mar 26, 2026Collaborator·

  ·
  2

• Remove broken code

  #580·CohenCyril opened Feb 25, 2026Member·

  ·

• Adapt to rocq-prover/rocq#21417

  #569·mattam82 opened Dec 19, 2025·

  ·
  1

• Drop 8.20 from CI

  #565·gares opened Oct 28, 2025Member·

  ·

• Add warning about implicitly local HB.instance calls, improve error messages

  #561·lweqx opened Oct 16, 2025·

  ·
  4

• Pglobal (wip adapt to algebraic universes)

  #545·CohenCyril opened Jul 1, 2025Member·

  ·

• [feat] support for multiple subjects

  #535·gares opened Apr 28, 2025Member·

  ·
  5

• fix test-suite rocq 9

  #534·gares opened Apr 28, 2025Member·

  ·

• mixin-instance-type->mixin-src does not use the typing information

  #521·Tragicus opened Mar 4, 2025Contributor·

  ·
  4

• Unify declare saturate

  #485·gares opened Dec 12, 2024Member·

  ·

• Instance before structure

  #475·gares opened Dec 11, 2024Member·

  ·

• fix #386

  #423·gares opened Jun 13, 2024Member·

  ·
  1

  7

• Generalized coercions

  #420·Tragicus opened May 28, 2024Contributor·

  ·
  42

• [refactor] instance declaration

  #376·gares opened Aug 1, 2023Member·3 of 5 tasks·

  ·
  24

• wrapper mixin step0

  #370·ptorrx opened Jun 19, 2023Collaborator·

  ·
  5

• Ongoing experiment with Iris hierarchy

  #364·CohenCyril opened Jun 14, 2023Member·

  ·

• test for step 0 of CoREACT

  #357·gares opened Jun 2, 2023Member·

  ·
  8

• Anomaly with universes for reverse_coercion symbol

  #350·CohenCyril opened Apr 18, 2023Member·

  ·
  4