-DEPOBJS = xml2Gdome.ml proofEngine.ml cic2Xml.ml cic2acic.ml \
- logicalOperations.ml sequentPp.ml gTopLevel.ml
+DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \
+ proofEngineReduction.ml proofEngineReduction.mli \
+ proofEngineStructuralRules.ml proofEngineStructuralRules.mli \
+ tacticals.ml tacticals.mli reductionTactics.ml reductionTactics.mli \
+ primitiveTactics.ml primitiveTactics.mli variousTactics.ml variousTactics.mli \
+ introductionTactics.ml introductionTactics.mli eliminationTactics.ml eliminationTactics.mli \
+ negationTactics.ml negationTactics.mli equalityTactics.ml equalityTactics.mli \
+ ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\
+ proofEngine.ml proofEngine.mli \
+ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
+ cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \
+ logicalOperations.mli sequentPp.ml sequentPp.mli mQueryGenerator.mli \
+ mQueryLevels.ml mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml gTopLevel.ml