diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-16 17:28:30 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-16 17:28:30 +0100 |
| commit | a65f9028c4834fe2ae803d1155780c1caf6790c4 (patch) | |
| tree | b988916f3c70fd87a3934ac9d6a97aeb042adc93 /test-suite/bugs/closed/3828.v | |
| parent | 811df9475898045b720f804c7d49638faa4e8478 (diff) | |
#3828 is solved.
Diffstat (limited to 'test-suite/bugs/closed/3828.v')
| -rw-r--r-- | test-suite/bugs/closed/3828.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3828.v b/test-suite/bugs/closed/3828.v new file mode 100644 index 000000000..ae11c6c96 --- /dev/null +++ b/test-suite/bugs/closed/3828.v @@ -0,0 +1,2 @@ +Goal 0 = 0. +Fail pose ?Goal. |