PACKAGE = cic_textual_parser2
REQUIRES = \
	helm-tactics helm-logger helm-cic_unification helm-cic_transformations \
	helm-pxp helm-utf8_macros \
	ulex
NOTATIONS = logic arit tex
# NOTATIONS = logic arit
INTERFACE_FILES = \
	disambiguateTypes.mli \
	disambiguateChoices.mli \
	cicTextualLexer2.mli \
	cicTextualParser2.mli \
	disambiguate.mli
IMPLEMENTATION_FILES = \
	$(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
	$(patsubst %,%_notation.ml,$(NOTATIONS))

all:

cicTextualLexer2.cmo: cicTextualLexer2.ml
	$(OCAMLC_P4) -c $<
cicTextualParser2.cmo: cicTextualParser2.ml
	$(OCAMLC_P4) -c $<
cicTextualLexer2.cmx: cicTextualLexer2.ml
	$(OCAMLOPT_P4) -c $<
cicTextualParser2.cmx: cicTextualParser2.ml
	$(OCAMLOPT_P4) -c $<

%_notation.cmo: %_notation.ml
	$(OCAMLC_P4) -c $<
%_notation.cmx: %_notation.ml
	$(OCAMLOPT_P4) -c $<

LOCAL_LINKOPTS = -package helm-cic_textual_parser2 -linkpkg
test: test_lexer test_parser
test_lexer: test_lexer.ml $(PACKAGE).cma
	$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
test_parser: test_parser.ml $(PACKAGE).cma
	$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<

clean: extra_clean
distclean: extra_clean
	rm -f macro_table.dump
extra_clean:
	rm -f test_lexer test_parser

include ../Makefile.common
OCAMLARCHIVEOPTIONS += -linkall

disambiguateTypes.cmi: disambiguateTypes.mli
	$(OCAMLC) -c -rectypes $<
disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi
	$(OCAMLC) -c -rectypes $<
disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi
	$(OCAMLOPT) -c -rectypes $<