diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common index b2581776a7..fa76dac60b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -321,6 +321,7 @@ PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ ALLVO:= $(THEORIESVO) $(PLUGINSVO) VFILES:= $(ALLVO:.vo=.v) +ALLSTDLIB := test-suite/misc/universes/all_stdlib # convert a (stdlib) filename into a module name: # remove .vo, replace theories and plugins by Coq, and replace slashes by dots |