From 6bee8342c0a914376688fba3927352f826aa9942 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 30 Nov 2011 10:36:22 +0000
Subject: Quick hack to avoid anomaly on using Program w/o having required
 JMeq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14749 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/ProgramWf.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 81bdbc29f0..00a13aed0c 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -1,3 +1,9 @@
+(* Before loading Program, check non-anomaly on missing library Program *)
+
+Fail Program Definition f n (e:n=n): {n|n=0} := match n,e with 0, refl => 0 | _, _ => 0 end.
+
+(* Then we test Program properly speaking *)
+
 Require Import Arith Program.
 Require Import ZArith Zwf.
 
-- 
cgit v1.2.3