From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 21 Jul 2005 20:40:10 +0000 (+0000)
Subject: added CicNotation.load_notation call to disambiguate terms
X-Git-Tag: V_0_7_2~116
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=575fd8b6044d87cd7116b0dc3cd695e790f7b152;p=helm.git

added CicNotation.load_notation call to disambiguate terms
---

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")