diff options
| author | Pierre-Marie Pédrot | 2015-01-27 20:14:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-27 20:14:09 +0100 |
| commit | 7ea6e6a3f10089f1ae8e1cb3be324edc39958c88 (patch) | |
| tree | dd1615414899248443091e1248141cb62af3a866 | |
| parent | 56a7a49927c3fb98b852db2f4b4f97d9cac3bf0d (diff) | |
Adding a test for bug #3957.
| -rw-r--r-- | test-suite/bugs/closed/3957.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3957.v b/test-suite/bugs/closed/3957.v new file mode 100644 index 0000000000..e20a6e97f0 --- /dev/null +++ b/test-suite/bugs/closed/3957.v @@ -0,0 +1,6 @@ +Ltac foo tac := tac. + +Goal True. +Proof. +foo subst. +Admitted. |