From f83ae8630b01c8a987a41d8bcf4184ff0290e1da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Aug 2016 12:21:14 +0200
Subject: [PATCH] Fix typo that I forgot to git commit --amend.

---
 proofmode/classes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofmode/classes.v b/proofmode/classes.v
index a01f96e06..83c1f2e7c 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -62,7 +62,7 @@ Global Arguments into_exist {_} _ _ {_}.
 Class IntoExceptLast (P Q : uPred M) := into_except_last : P ⊢ ◇ Q.
 Global Arguments into_except_last : clear implicits.
 
-Class IsExpectLast (Q : uPred M) := is_except_last : ◇ Q ⊢ Q.
+Class IsExceptLast (Q : uPred M) := is_except_last : ◇ Q ⊢ Q.
 Global Arguments is_except_last : clear implicits.
 
 Class FromVs (P Q : uPred M) := from_vs : (|=r=> Q) ⊢ P.
-- 
GitLab