TEST_REQUIRES = \
helm-registry \
- helm-mathql_interpreter \
- helm-mathql_generator \
helm-tactics \
helm-cic_transformations \
helm-cic_textual_parser2 \
- helm-cic_textual_parser \
- helm-tex_cic_textual_parser \
+ helm-mathql_interpreter \
+ helm-mathql_generator \
+ helm-xmldiff \
+ lablgtk2 \
mathml-editor \
- lablgtkmathview
+ lablgtkmathview \
+ mysql
-REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs
+REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade
-PREDICATES = "gnome,init,glade"
OCAMLOPTIONS = \
-package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread
-OCAMLFIND = ocamlfind
+OCAMLFIND = @OCAMLFIND@
OCAMLDEBUGOPTIONS = -g
OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS)
OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS)
INTERFACE_FILES = \
proofEngine.mli \
logicalOperations.mli \
- oldDisambiguate.mli \
disambiguatingParser.mli \
termEditor.mli \
texTermEditor.mli \
- xmlDiff.mli \
- chosenTransformer.mli \
termViewer.mli \
invokeTactics.mli \
hbugs.mli \
TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo
TESTOBJS = \
- oldDisambiguate.cmo \
disambiguatingParser.cmo \
batchParser.cmo
REGTESTOBJS = $(TESTOBJS) regtest.cmo
./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
librarytest.opt: testlibrary.opt
./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG
+typecheck_uri: typecheck_uri.ml
+ $(OCAMLFIND) ocamlc -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
+typecheck_uri.opt: typecheck_uri.ml
+ $(OCAMLFIND) opt -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
MAIN = ./gTopLevel
ARGS =