From c5d171bd4131c6101b4bd48e6132d65b73bb0bff Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 Feb 2004 11:42:25 +0000 Subject: [PATCH] eqT removed. --- helm/ocaml/cic_disambiguation/logic_notation.ml | 13 ------------- 1 file changed, 13 deletions(-) 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" -- 2.39.2