Porting URIs to V8.0.

[helm.git] / helm / ocaml / cic_disambiguation / arit_notation.ml

diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml
index 51faaa6acc06a91e6cc1d400e661b92217c203a1..324501eb31055db58aab1d8f4f70a1dc4db440d2 100644 (file)
--- a/helm/ocaml/cic_disambiguation/arit_notation.ml
+++ b/helm/ocaml/cic_disambiguation/arit_notation.ml
@@ -120,16 +120,3 @@ let _ =
           Cic.Appl [
             Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
               Cic.Implicit (Some `Type); t1; t2 ] ]));
-  DisambiguateChoices.add_symbol_choice "neq"
-    ("not equal to (sort Type)",
-      (fun env _ args ->
-        let t1, t2 =
-          match args with
-          | [t1; t2] -> t1, t2
-          | _ -> raise DisambiguateChoices.Invalid_choice
-        in
-        Cic.Appl [ const HelmLibraryObjects.Logic.not_URI;
-          Cic.Appl [
-            Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []);
-              Cic.Implicit (Some `Type); t1; t2 ] ]));
-