diff options
| -rw-r--r-- | contrib/extraction/test/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index 14fdf6fdfd..89f13c75bd 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -10,6 +10,7 @@ AXIOMSVO:= \ theories/Arith/Arith.vo \ theories/Lists/List.vo \ theories/Reals/% \ +theories/Num/% \ theories/Relations/Rstar.vo \ theories/Sets/Integers.vo \ theories/ZArith/Zsyntax.vo @@ -78,7 +79,6 @@ $(REALSML): realsml # Utilities # - ml2v: ml2v.ml ocamlc -o $@ $< |