BIN_DIR = /usr/local/bin
REQUIRES = helm-cic_proof_checking http
PREDICATES =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
-OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -g
-OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes
+ifeq ($(origin OCAMLPATH), undefined)
+OCAMLFIND = OCAMLPATH=../../components/METAS ocamlfind
+else
+OCAMLFIND = ocamlfind
+endif
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) -g
+OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
OCAMLDEP = ocamldep
-LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
-LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
all: $(PROOFCHECKEROBJS) proofChecker
opt: $(PROOFCHECKEROBJS:.cmo=.cmx) proofChecker.opt