Commit 238d31bf authored by Robbert Krebbers's avatar Robbert Krebbers

Fix order of imports.

This fixes a bug in 916ff44a causing proof mode notations not being
pretty printed.
parent 485ef65e
Pipeline #1790 passed with stage
From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns. From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
From iris.algebra Require Export upred. From iris.algebra Require Export upred.
From iris.proofmode Require Export notation classes. From iris.proofmode Require Export classes notation.
From iris.prelude Require Import stringmap hlist. From iris.prelude Require Import stringmap hlist.
Declare Reduction env_cbv := cbv [ Declare Reduction env_cbv := cbv [
......
From iris.proofmode Require Import tactics notation. From iris.proofmode Require Import tactics.
From iris.proofmode Require Import pviewshifts invariants. From iris.proofmode Require Import pviewshifts invariants.
Lemma demo_0 {M : ucmraT} (P Q : uPred M) : Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
......
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