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/coqdoc/bug5648.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 test-suite/coqdoc/bug5648.v (limited to 'test-suite/coqdoc/bug5648.v') diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v new file mode 100644 index 00000000..9b62dd1e --- /dev/null +++ b/test-suite/coqdoc/bug5648.v @@ -0,0 +1,19 @@ +Lemma a : True. +Proof. +auto. +Qed. + +Variant t := +| A | Add | G | Goal | L | Lemma | P | Proof . + +Definition d x := + match x with + | A => 0 + | Add => 1 + | G => 2 + | Goal => 3 + | L => 4 + | Lemma => 5 + | P => 6 + | Proof => 7 + end. -- cgit v1.2.3