From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 26 Feb 2004 11:42:25 +0000 (+0000)
Subject: eqT removed.
X-Git-Tag: v0_0_4~78
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5d171bd4131c6101b4bd48e6132d65b73bb0bff;p=helm.git

eqT removed.
---

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"