From bfa14514cb671b6e393104ce98628af43ae94c4b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 9 Jan 2006 12:33:13 +0000 Subject: [PATCH] ignoring the result of load_notation --- helm/ocaml/paramodulation/saturate_main.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index e65af7eed..bec597645 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -143,8 +143,8 @@ let _ = ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; -CicNotation2.load_notation [] core_notation_script; -CicNotation2.load_notation [] "../../matita/coq.ma"; +ignore (CicNotation2.load_notation [] core_notation_script); +ignore (CicNotation2.load_notation [] "../../matita/coq.ma"); let dbd = HMysql.quick_connect ~host:(Helm_registry.get "db.host") ~user:(Helm_registry.get "db.user") -- 2.39.2