universes are saved to disk

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 365f947c001a5c163efa811d046797c36d12197a..707e31d988fff576c60795d8a257b6f1ec380179 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -580,7 +580,7 @@ let eval_coercion status coercion =
     (* also adds them to the Db *)
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
   let status =
-   List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
+   List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
     status new_coercions in
   let statement_of name =
     GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,