Commit 18f29711 authored by Ralf Jung's avatar Ralf Jung

don't use Proof Using in a few files that get too many unnecessary annotations from this

parent 3c70bf99
Pipeline #3578 passed with stage
in 10 minutes and 39 seconds
From iris.algebra Require Export ofe.
Set Default Proof Using "Type*".
(* FIXME: This file needs a 'Proof Using' hint, but the default we use
everywhere makes for lots of extra ssumptions. *)
Record solution (F : cFunctor) := Solution {
solution_car :> ofeT;
......
From iris.prelude Require Export set.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Set Default Proof Using "Type*".
(* FIXME: This file needs a 'Proof Using' hint, but the default we use
everywhere makes for lots of extra ssumptions. *)
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
......
  • The affected lemmas in cofe_solverare internal, so should never be referred to. It should not matter there.

  • The problematic sts file is base_logic/lib/sts. I have fixed that one 53f6857f.

    Considering my previous remark about cofe_solver, I think this commit can be undone.

Markdown is supported
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