From 575fd8b6044d87cd7116b0dc3cd695e790f7b152 Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
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