do not use tex notation per default (used only by tex term editor)

diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile
index ef4ff8cc260aaf6dc570572b8d7b9e5cb69c223a..ea516c526930d5c4144ab0ccdac8477861f1e2af 100644 (file)
--- a/helm/ocaml/cic_disambiguation/Makefile
+++ b/helm/ocaml/cic_disambiguation/Makefile
@@ -3,7 +3,8 @@ PACKAGE = cic_textual_parser2
 REQUIRES = \
        helm-tactics helm-logger helm-cic_unification helm-cic_transformations \
        ulex pxp camlp4.gramlib
-NOTATIONS = logic arit tex
+# NOTATIONS = logic arit tex
+NOTATIONS = logic arit
 INTERFACE_FILES = \
        disambiguateTypes.mli \
        disambiguateChoices.mli \