From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/bugs/closed/4603.v | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 test-suite/bugs/closed/4603.v (limited to 'test-suite/bugs/closed/4603.v') diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v new file mode 100644 index 00000000..e7567623 --- /dev/null +++ b/test-suite/bugs/closed/4603.v @@ -0,0 +1,10 @@ +Axiom A : Type. + +Goal True. exact I. +Check (fun P => P A). +Abort. + +Goal True. +Definition foo (A : Type) : Prop:= True. + set (x:=foo). split. +Qed. \ No newline at end of file -- cgit v1.2.3