- new generated query "unreferred" implemented at server side

[helm.git] / helm / gTopLevel / Makefile

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 6dfa38622896000f116052ff92564176b37232fb..e449673058fbdb9d8d9aa028f2e9ff0f2dd6a527 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -26,7 +26,7 @@ DEPOBJS = \
         gTopLevel.ml
 
 TOPLEVELOBJS = \
-                  doubleTypeInference.cmo eta_fixing.cmo content2cic.cmo \
+            eta_fixing.cmo content2cic.cmo \
              proofEngine.cmo logicalOperations.cmo \
              disambiguate.cmo termEditor.cmo texTermEditor.cmo termViewer.cmo \
              invokeTactics.cmo hbugs.cmo gTopLevel.cmo