]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/logic_notation.ml
Porting URIs to V8.0.
[helm.git] / helm / ocaml / cic_disambiguation / logic_notation.ml
index 885cc214058e43be72c58595497b6f35e8780022..f622ce034e8312b59609807cb6c88b9a7d34f0a9 100644 (file)
@@ -74,7 +74,7 @@ let _ =
          | _ -> raise DisambiguateChoices.Invalid_choice
        in
        Cic.Appl [
-         Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []);
+         Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
            Cic.Implicit (Some `Type); t1; t2
        ]));
   DisambiguateChoices.add_binary_op "and" "logical and"