Commit 2c6549f0 authored by MARCHE Claude's avatar MARCHE Claude

Prover example: Nat module does not needed to be extracted

parent 6589d1dc
......@@ -20,8 +20,6 @@ ifeq ($(BENCH),yes)
endif
MLWUTIL=Nat
MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
Firstorder_formula_impl Firstorder_formula_list_impl \
Firstorder_tableau_impl Unification FormulaTransformations \
......@@ -30,10 +28,9 @@ MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
MLWIMPL=$(MLWTYPES) ProverMain ProverTest
BD=build
MLUTIL=$(patsubst %,$(BD)/%__Nat,$(MLWUTIL))
MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLWTYPES))
MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLWIMPL))
MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
MLALL=$(MLTYPES) $(MLIMPL)
ML=$(patsubst %,%.ml,$(MLALL))
CMX=$(patsubst %,%.cmx,$(MLALL))
OCAMLC=ocamlopt.opt
......
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