From f5923c2174fbb419397f127af31ab1cd0b223e0a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 31 Jan 2017 06:36:25 +0100 Subject: Fixing #5311 (anomaly on unexpected intro pattern). This was introduced in 8.5 while reorganizing the structure of intro-patterns. --- test-suite/bugs/closed/5331.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/5331.v (limited to 'test-suite/bugs/closed/5331.v') diff --git a/test-suite/bugs/closed/5331.v b/test-suite/bugs/closed/5331.v new file mode 100644 index 000000000..0d72fcb5d --- /dev/null +++ b/test-suite/bugs/closed/5331.v @@ -0,0 +1,11 @@ +(* Checking no anomaly on some unexpected intropattern *) + +Ltac ih H := induction H as H. +Ltac ih' H H' := induction H as H'. + +Goal True -> True. +Fail intro H; ih H. +intro H; ih' H ipattern:[]. +exact I. +Qed. + -- cgit v1.2.3