Skip to content

GitLab

I
Iris
Commit 7c00020b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Kill dependency of `base_logic` on `proofmode` to speed up compilation.

parent 40370710
Pipeline #7007 passed with stage
    in 15 minutes and 13 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 0 additions and 1 deletion
    theories/base_logic/base_logic.v
    View file @ 7c00020b
    From iris.base_logic Require Export derived. From iris.base_logic Require Export derived.
    From iris.bi Require Export bi. From iris.bi Require Export bi.
    From iris.proofmode Require Import tactics.
    From iris.algebra Require Import proofmode_classes. From iris.algebra Require Import proofmode_classes.
    Set Default Proof Using "Type". Set Default Proof Using "Type".
    ......
    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