Commit b2ca71c0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Do no longer play tricks with headers of Coq realizations.

parent 2de30b06
......@@ -1020,7 +1020,7 @@ ifeq (@enable_coq_fp_libs@,yes)
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
endif
update-coq: remove-coq-headers update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float headers-coq
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
......@@ -2031,23 +2031,16 @@ dist: $(MORE_DIST)
# file headers
###############
headers: headers-coq
headers:
headache -c misc/headache_config.txt -h misc/header.txt \
Makefile.in configure.in \
src/*/*.ml src/*/*.ml[iyl4] \
plugins/*/*.ml plugins/*/*.ml[ily] \
lib/coq-tactic/*.v lib/coq/*.v \
lib/coq-tactic/*.v lib/coq/*.v lib/coq/*/*.v \
src/server/*.c src/server/*.h \
src/ide/resetgc.c \
examples/use_api/*.ml
headers-coq:
headache -c misc/headache_config.txt -h misc/header.txt \
lib/coq/*/*.v
remove-coq-headers:
headache -r -c misc/headache_config.txt lib/coq/*/*.v
#########
# myself
#########
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment