From 4d779fe8ff9c2b81eddb671dc0e60d3743357ce5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 8 Apr 2014 12:57:17 +0200
Subject: Retype application of fix_proto to get the right universes in Program

---
 test-suite/bugs/closed/1784.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/1784.v b/test-suite/bugs/closed/1784.v
index fb2f0ca90e..0b63d7b567 100644
--- a/test-suite/bugs/closed/1784.v
+++ b/test-suite/bugs/closed/1784.v
@@ -92,7 +92,7 @@ Next Obligation. intro H; inversion H; subst. Defined.
 Next Obligation.
   intro H1; contradict H. inversion H1; subst. assumption.
   contradict H0; assumption. Defined.
-Next Obligation.
+Next Obligation. 
   intro H1; contradict H0. inversion H1; subst. assumption. Defined.
 Next Obligation.
   intro H1; contradict H. inversion H1; subst. assumption. Defined.
-- 
cgit v1.2.3