diff options
Diffstat (limited to 'test-suite/coqdoc/bug5648.v')
-rw-r--r-- | test-suite/coqdoc/bug5648.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v new file mode 100644 index 000000000..353ecc49a --- /dev/null +++ b/test-suite/coqdoc/bug5648.v @@ -0,0 +1,24 @@ +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. + +Ltac Next := easy. + +Lemma yes : True. +Proof. Next. Qed. |