diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-19 13:17:08 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-19 13:20:21 +0200 |
commit | fa1e921257735d246d04be9e456f11ec7330b37a (patch) | |
tree | 2b857e5147e2b9e7b42997ad90f483e67d809593 /theories/Lists/ListTactics.v | |
parent | 9f11adda4bff194a3c6a66d573ce7001d4399886 (diff) |
Re-adding explicit dependency of misc universe test into all_stdlib.v.
Was working when calling test-suite from main Makefile but not when
calling directly from the test-suite Makefile.
The dependency was mistakenly dropped in 98a927aef.
Diffstat (limited to 'theories/Lists/ListTactics.v')
0 files changed, 0 insertions, 0 deletions