diff options
| author | Gaëtan Gilbert | 2017-09-21 00:53:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-25 14:18:35 +0100 |
| commit | 765392492df2f5e065b2b5e706b6620846337cc0 (patch) | |
| tree | ccf14d9040e76acca2a902cdefa57fefc53bc64a /test-suite/Makefile | |
| parent | 280c922fc55b57c430cad721c83650a796a375fd (diff) | |
Universe binders survive sections, modules and compilation.
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f169f86e88..6865dcc768 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -95,7 +95,8 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile PREREQUISITELOG = prerequisite/admit.v.log \ - prerequisite/make_local.v.log prerequisite/make_notation.v.log + prerequisite/make_local.v.log prerequisite/make_notation.v.log \ + prerequisite/bind_univs.v.log ####################################################################### # Phony targets |