X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Flogic_notation.ml;h=192c2a9c1c96553aa139654489e6df1d90c6adc5;hb=c5d171bd4131c6101b4bd48e6132d65b73bb0bff;hp=f622ce034e8312b59609807cb6c88b9a7d34f0a9;hpb=a6be2877b7ed9c9add7060ea853206d5b7d0d673;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
index f622ce034..192c2a9c1 100644
--- 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"