]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/Makefile
* doubleTypeInference.ml* added. For now, it just computes the synthesized type.
[helm.git] / helm / gTopLevel / Makefile
index 44c9887f77da93bef40a146ef523bb8a09203f9a..8a9c5e535792782c06f68609b80692f447ca2a06 100644 (file)
@@ -15,12 +15,13 @@ all: gTopLevel
 opt: gTopLevel.opt
 
 DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \
-          cic2acic.ml cic2acic.mli logicalOperations.ml sequentPp.ml \
-          mquery.mli mquery.ml gTopLevel.ml
+          doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
+          cic2acic.mli logicalOperations.ml sequentPp.ml mquery.mli \
+          mquery.ml gTopLevel.ml
 
 TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \
-               cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \
-               mquery.cmo gTopLevel.cmo
+               cic2Xml.cmo doubleTypeInference.cmo cic2acic.cmo \
+               logicalOperations.cmo sequentPp.cmo mquery.cmo gTopLevel.cmo
 
 depend:
        $(OCAMLDEP) $(DEPOBJS) > .depend