Correct error message in proof docs

idris-lang · Mar 23, 2015 · 9f4aea3 · 9f4aea3
1 parent be93168
commit 9f4aea3
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/docs/proofs/pluscomm.rst b/docs/proofs/pluscomm.rst
@@ -88,9 +88,9 @@ error:
 
     When elaborating right hand side of four_eq_five:
     Can't unify
-            5 = 5
+            x = x (Type of Refl)
     with
-            4 = 5
+            4 = 5 (Expected type)
 
 Type checking equality proofs
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~