aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index a12559090..2aa10f5c6 100644
--- a/Makefile
+++ b/Makefile
@@ -91,7 +91,7 @@ UNBOXEDVALUES= # is "-unboxed-values" to use unboxed values
COQOPTS=$(GLOB) $(COQ_XML) $(VM) $(UNBOXEDVALUES)
TIME= # is "'time -p'" to get compilation time of .v
-BOOTCOQTOP= $(TIME) $(BESTCOQTOP) -boot $(COQOPTS)
+BOOTCOQTOP= $(TIME) $(BESTCOQTOP) -boot $(COQOPTS)
###########################################################################
@@ -141,7 +141,7 @@ LIBRARY=\
PRETYPING=\
pretyping/termops.cmo pretyping/evd.cmo \
- pretyping/reductionops.cmo pretyping/inductiveops.cmo \
+ pretyping/reductionops.cmo pretyping/vnorm.cmo pretyping/inductiveops.cmo \
pretyping/retyping.cmo pretyping/cbv.cmo \
pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \
pretyping/tacred.cmo \