From 575fd8b6044d87cd7116b0dc3cd695e790f7b152 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 21 Jul 2005 20:40:10 +0000 Subject: [PATCH] added CicNotation.load_notation call to disambiguate terms --- helm/ocaml/paramodulation/saturate_main.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index c9eec5e46..05d2cd047 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -1,5 +1,7 @@ let configuration_file = ref "../../matita/matita.conf.xml";; +let core_notation_script = "../../matita/core_notation.ma";; + let get_from_user ~(dbd:Mysql.dbd) = let rec get () = match read_line () with @@ -42,6 +44,7 @@ let _ = ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; +CicNotation.load_notation core_notation_script; let dbd = Mysql.quick_connect ~host:(Helm_registry.get "db.host") ~user:(Helm_registry.get "db.user") -- 2.39.2