Skip to content
Snippets Groups Projects
Commit 24cc2e47 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use simple apply in f_equiv and solve_proper. 

As suggested by Pierre-Marie Pédrot in the Coq-club thread:

  [Coq-Club] Very slow failing apply

To work arround some performance issues in Iris.
parent 7891aa0b
No related branches found
No related tags found
Checking pipeline status
Hide whitespace changes
Inline Side-by-side
Showing
with 22 additions and 22 deletions
  • Ralf Jung @jung ·
    Owner

    Upgrading to latest Iris breaks lambda-rust: A solve_type_proper that used to work now fails. My first guess is that this commit broke it.

    Cc @jjourdan @robbertkrebbers

  • Ralf Jung @jung ·
    Owner

    Never mind, it was a different problem.

0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment