Skip to content

6 packages from rocq-community/trocq at 0.4.0 - #3761

Open
CohenCyril wants to merge 3 commits into
rocq-prover:masterfrom
CohenCyril:opam-publish-coq-trocq-dev.0.4.0
Open

6 packages from rocq-community/trocq at 0.4.0#3761
CohenCyril wants to merge 3 commits into
rocq-prover:masterfrom
CohenCyril:opam-publish-coq-trocq-dev.0.4.0

Conversation

@CohenCyril

Copy link
Copy Markdown
Contributor

This pull-request concerns:

  • coq-trocq.0.4.0: A modular parametricity plugin for proof transfer in Coq
  • coq-trocq-dev.0.4.0: A modular parametricity plugin for proof transfer in Coq
  • coq-trocq-hott.0.4.0: A modular parametricity plugin for proof transfer in Coq
  • coq-trocq-hott-examples.0.4.0: A modular parametricity plugin for proof transfer in Coq: examples
  • coq-trocq-std.0.4.0: A modular parametricity plugin for proof transfer in Coq
  • coq-trocq-std-examples.0.4.0: A modular parametricity plugin for proof transfer in Coq: examples


🐫 Pull-request generated by opam-publish v2.7.1

@SkySkimmer

Copy link
Copy Markdown
Contributor

I see

- File "./generic/Param_list.v", line 20, characters 0-17:
- Error: Universe polymorphic gref list used with the 'global' term constructor
- 
- File "./generic/Param_nat.v", line 19, characters 0-16:
- Error: Universe polymorphic gref nat used with the 'global' term constructor

@gares

gares commented Jul 30, 2026

Copy link
Copy Markdown
Member

Is the discrepancy in the rocq upper bound an oversight?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants