diff options
Diffstat (limited to 'test-suite/coqdoc/bug5648.v')
-rw-r--r-- | test-suite/coqdoc/bug5648.v | 19 |
1 files changed, 19 insertions, 0 deletions
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. |