From fb4d4d72b9c1570a7e6d9cb1e8ffb0f61b90c5f2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 4 Jun 2010 10:46:57 +0000
Subject: Backported r13068 to branch v8.3 (whd_betaiota on inferred return
 match predicate) and fixed Notation.out test accordingly.

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

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 01eef8082b..924030bac2 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -1,7 +1,7 @@
 true ? 0; 1
      : nat
 if true as x return (x ? nat; bool) then 0 else true
-     : true ? nat; bool
+     : nat
 Defining 'proj1' as keyword
 fun e : nat * nat => proj1 e
      : nat * nat -> nat
-- 
cgit v1.2.3