From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/closed/4527.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'test-suite/bugs/closed/4527.v') diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 08628377..117d6523 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -1,10 +1,11 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1199 lines to 430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, then from 269 lines to 255 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. -- cgit v1.2.3