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/HoTT_coq_123.v | 1 + 1 file changed, 1 insertion(+) (limited to 'test-suite/bugs/closed/HoTT_coq_123.v') diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index 994dff63..6ee6e653 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") *) (* File reduced by coq-bug-finder from original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *) Set Universe Polymorphism. -- cgit v1.2.3