FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 9b454f29429647d6a4bb6202ae6e4a6b7357d382..bb01585d12ce603108b7948dcdad09082a57ac31 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -470,16 +470,22 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
   GrafiteAst.Coercion
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
+let basic_eval_unification_hint (t,n) status =
+ let hstatus =
+  NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
+ in
+  { status with NRstatus.uhint_db = hstatus }
+;;
+
+let inject_unification_hint =
+ NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
+;;
+
 let eval_unification_hint status t n = 
- let aux status =
-  let hstatus =
-   NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
-  in
-   { status with NRstatus.uhint_db = hstatus } in
- let rstatus = aux (GrafiteTypes.get_rstatus status) in
+ let rstatus =
+  basic_eval_unification_hint (t,n) (GrafiteTypes.get_rstatus status) in
  let status = GrafiteTypes.set_rstatus rstatus status in
- let dump = GrafiteTypes.get_dump status in
- let dump = fun status -> aux (dump status) in
+ let dump = inject_unification_hint (t,n)::(GrafiteTypes.get_dump status) in
  let status = GrafiteTypes.set_dump dump status in
   status,`Old []
 ;;
@@ -736,7 +742,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      let status = eval_from_moo.efm_go status moopath in
      let rstatus = GrafiteTypes.get_rstatus status in
      let rstatus =
-      NCicLibrary.require ~baseuri:(NUri.uri_of_string baseuri) rstatus in
+      NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) rstatus
+     in
      let status = GrafiteTypes.set_rstatus rstatus status in
 (* debug
      let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in