]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/Makefile
Added a filter for uris in tactic "auto".
[helm.git] / helm / ocaml / tactics / Makefile
index b5430999e32a801d82b6472679d5532760800b73..36c81117f5e2d5b6a46ff916f1c69eddf59cc774 100644 (file)
@@ -4,12 +4,14 @@ REQUIRES = \
        helm-cic_unification helm-mathql_interpreter helm-mathql_generator
 
 INTERFACE_FILES = \
+       newConstraints.mli match_concl.mli filter_auto.mli\
        proofEngineReduction.mli proofEngineHelpers.mli \
+       newConstraints.mli match_concl.mli \
        tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
        primitiveTactics.mli tacticChaser.mli variousTactics.mli \
        introductionTactics.mli eliminationTactics.mli negationTactics.mli \
        equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \
-       fourierR.mli
+       fourierR.mli statefulProofEngine.mli
 IMPLEMENTATION_FILES = proofEngineTypes.ml $(INTERFACE_FILES:%.mli=%.ml)
 
 include ../Makefile.common