X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_engine%2FgrafiteEngine.ml;h=65dd17b6a096c1e144daf7068e80cf49cba2ce2d;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=60b2b6a9dbe08935058edbd75244ec0854d7aa17;hpb=b1527286e32c8651d65619af61e3f638b3b89f8d;p=helm.git

diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml
index 60b2b6a9d..65dd17b6a 100644
--- a/helm/ocaml/grafite_engine/grafiteEngine.ml
+++ b/helm/ocaml/grafite_engine/grafiteEngine.ml
@@ -397,6 +397,7 @@ let coercion_moo_statement_of uri =
 let eval_coercion status ~add_composites uri =
  let basedir = Helm_registry.get "matita.basedir" in
  let status,compounds =
+   prerr_endline "evaluating a coercion command";
   GrafiteSync.add_coercion ~basedir ~add_composites status uri in
  let moo_content = coercion_moo_statement_of uri in
  let status = GrafiteTypes.add_moo_content [moo_content] status in
@@ -522,18 +523,14 @@ let add_coercions_of_record_to_moo obj lemmas status =
                 None) 
             lemmas)
       in
+      prerr_endline "actual coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
         coercions;
-      let status = GrafiteTypes.add_moo_content moo_content status in
-      let basedir = Helm_registry.get "matita.basedir" in
-      List.fold_left 
-        (fun (status,lemmas) uri ->
-          let status,new_lemmas =
-           GrafiteSync.add_coercion ~basedir ~add_composites:true status uri
-          in
-           status,new_lemmas@lemmas
-        ) (status,[]) coercions
+      let status = GrafiteTypes.add_moo_content moo_content status in 
+      {status with 
+        GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, 
+      lemmas
 
 let add_obj uri obj status =
  let basedir = Helm_registry.get "matita.basedir" in