@@ -713,7 +713,7 @@ endif
713713# ########## Targets ##########
714714
715715default_target : vst $(PROGSDIR )
716- vst : _CoqProject msl veric floyd simpleconc
716+ vst : _CoqProject msl veric ora floyd simpleconc
717717
718718ifeq ($(BITSIZE ) ,64)
719719test : vst progs64
@@ -740,6 +740,8 @@ files: _CoqProject $(FILES:.v=.vo)
740740#
741741simpleconc : concurrency/conclib.vo atomics/verif_lock.vo
742742msl : _CoqProject $(MSL_FILES:%.v=msl/%.vo )
743+ ora : _CoqProject
744+ cd ora; $(MAKE )
743745sepcomp : _CoqProject $(CC_TARGET ) $(SEPCOMP_FILES:%.v=sepcomp/%.vo )
744746concurrency : _CoqProject $(CC_TARGET ) $(SEPCOMP_FILES:%.v=sepcomp/%.vo ) $(CONCUR_FILES:%.v=concurrency/%.vo )
745747linking : _CoqProject $(LINKING_FILES:%.v=linking/%.vo )
@@ -889,6 +891,7 @@ clean:
889891 rm -f $(addprefix veric/version., v vo vos vok glob) .lia.cache .nia.cache floyd/floyd.coq .depend _CoqProject _CoqProject-export $(wildcard * /.* .aux) $(wildcard * /* .glob) $(wildcard * /* .vo * /* .vos * /* .vok) compcert/* /* .{vo,vos,vok} compcert/* /* /* .{vo,vos,vok} compcert_new/* /* .{vo,vos,vok} compcert_new/* /* /* .{vo,vos,vok}
890892 rm -f progs/VSUpile/{* ,* /* }.{vo,vos,vok,glob}
891893 rm -f progs/memmgr/* .{vo,vos,vok,glob}
894+ rm -f ora/theories/* /* .{vo,vos,vok,glob}
892895 rm -f coq-ext-lib/theories/* .{vo,vos,vok,glob} InteractionTrees/theories/{* ,* /* }.{vo,vos,vok,glob}
893896 rm -f paco/src/* .{vo,vos,vok,glob}
894897 rm -f fcf/src/FCF/* .{vo,vos,vok,glob}
0 commit comments