From 238d31bf8ca873184a8c70a033a5b012198acb6a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Jun 2016 12:57:31 +0200
Subject: [PATCH] Fix order of imports.
This fixes a bug in 916ff44a causing proof mode notations not being
pretty printed.
---
proofmode/tactics.v | 2 +-
tests/proofmode.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 72dacaf19..a3de35f17 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
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.
Declare Reduction env_cbv := cbv [
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 6b7697cb8..67eee7e4d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics notation.
+From iris.proofmode Require Import tactics.
From iris.proofmode Require Import pviewshifts invariants.
Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
--
GitLab