From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- test-suite/bugs/closed/3382.v | 1 + 1 file changed, 1 insertion(+) (limited to 'test-suite/bugs/closed/3382.v') diff --git a/test-suite/bugs/closed/3382.v b/test-suite/bugs/closed/3382.v index 1d8e9167..3e374d90 100644 --- a/test-suite/bugs/closed/3382.v +++ b/test-suite/bugs/closed/3382.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines, then from 139 lines to 114 lines, then from 93 lines to 77 lines *) Set Implicit Arguments. -- cgit v1.2.3