eqT removed.

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
index f622ce034e8312b59609807cb6c88b9a7d34f0a9..192c2a9c1c96553aa139654489e6df1d90c6adc5 100644 (file)
--- a/helm/ocaml/cic_disambiguation/logic_notation.ml
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -64,19 +64,6 @@ let _ =
        Cic.Appl [
          Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
            Cic.Implicit (Some `Type); t1; t2
-       ]));
-  DisambiguateChoices.add_symbol_choice "eq"
-    ("equality over objects with sort Type",
-     (fun interp _ args ->
-       let t1, t2 =
-         match args with
-         | [t1; t2] -> t1, t2
-         | _ -> raise DisambiguateChoices.Invalid_choice
-       in
-       Cic.Appl [
-         Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
-           Cic.Implicit (Some `Type); t1; t2
-       ]));
   DisambiguateChoices.add_binary_op "and" "logical and"
     (mutind HelmLibraryObjects.Logic.and_URI);
   DisambiguateChoices.add_binary_op "or" "logical or"