Skip to content

Termops.Internal env printing functions take an evar map #18603

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Feb 4, 2024
Merged

Termops.Internal env printing functions take an evar map #18603

merged 1 commit into from
Feb 4, 2024

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Feb 1, 2024 •
edited
Loading

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 1, 2024
@SkySkimmer SkySkimmer requested review from a team as code owners February 1, 2024 12:51
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 1, 2024
@SkySkimmer SkySkimmer mentioned this pull request Feb 1, 2024
Closed
@SkySkimmer SkySkimmer added kind: fix This fixes a bug or incorrect documentation. request: full CI Use this label when you want your next push to trigger a full CI. labels Feb 2, 2024
SkySkimmer added a commit to SkySkimmer/Coq-Equations that referenced this pull request Feb 2, 2024
@SkySkimmer
Adapt to rocq-prover/rocq#18603 (print_rel_context takes evar map)
96b2d31
SkySkimmer added a commit to SkySkimmer/paramcoq that referenced this pull request Feb 2, 2024
@SkySkimmer
Adapt to rocq-prover/rocq#18603 (print_rel_context takes evar map)
a8b8529
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 2, 2024
@ppedrot ppedrot self-assigned this Feb 2, 2024
@JasonGross
Copy link
Member

Is this also going to fix the issue where Info sometimes gives anomalies (sorry, I don't have a reproducing example at the moment)

@SkySkimmer
Copy link
Contributor Author

Probably not, this doesn't seem to have changed the Info code

@ppedrot ppedrot added this to the 8.20+rc1 milestone Feb 4, 2024
@ppedrot
Copy link
Member

ppedrot commented Feb 4, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 39ea627 into rocq-prover:master Feb 4, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Feb 4, 2024

@ppedrot: Please take care of the following overlays:

  • 18603-SkySkimmer-temrops-use-evd.sh

ppedrot added a commit to rocq-community/paramcoq that referenced this pull request Feb 4, 2024
@ppedrot
Merge pull request #119 from SkySkimmer/temrops-use-evd
5b5ac50 
Adapt to rocq-prover/rocq#18603 (print_rel_context takes evar map)
ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Feb 4, 2024
@ppedrot
Merge pull request #581 from SkySkimmer/temrops-use-evd
7296932 
Adapt to rocq-prover/rocq#18603 (print_rel_context takes evar map)
@SkySkimmer SkySkimmer deleted the temrops-use-evd branch February 5, 2024 11:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@herbelin herbelin herbelin approved these changes

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

uncaught Not_found on ltac backtrace trace
4 participants
@SkySkimmer @JasonGross @ppedrot @herbelin