added coercions to Prod

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 61d69cbb9ace3b7770692205870fd840749e29b2..20fee8c181b3e2b2835942a3f4f6555a8e30f755 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -568,16 +568,9 @@ let eval_coercion status coercion =
   in
   let ty_src,ty_tgt = extract_last_two_p coer_ty in
   let context = [] in 
-  let src_uri = 
-    let ty_src = CicReduction.whd context ty_src in
-     CicUtil.uri_of_term ty_src
-  in
-  let tgt_uri = 
-    let ty_tgt = CicReduction.whd context ty_tgt in
-     CicUtil.uri_of_term ty_tgt
-  in
+  let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_src) in
+  let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_tgt) in
   let new_coercions =
-    (* 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,_) -> MatitaSync.add_obj uri o status)