From ae1fed6bd9bbb175456f8f5ffc7ada0abc455896 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 Dec 2008 17:34:22 +0000
Subject: Miscellaneous fixes and improvements: - Fixed a virtual bug of
 unification (ever occurs if w_unify called with   a non-empty context of
 rel's, which is a priori uncommon). - Fixed Notation.out test. - Add better
 coqide error message in case editor is called on an unnamed file.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations.out | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index acfcd5aff0..428583047d 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -50,6 +50,7 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
+Defining 'I' as keyword
 (false && I 3)%bool /\ I 6
      : Prop
 [|1, 2, 3; 4, 5, 6|]
-- 
cgit v1.2.3