- Changed ApplyTransformation API to return both the mathml and acic,

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index fe70f250aa89999161824cf26d08639dc18739a7..d8b822d82cf6f6b39287025869e22bef114a7482 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -52,7 +52,7 @@ let look_for_coercion src tgt =
   then
     begin
     prerr_endline "TROVATA coercion";
-    Some (CicUtil.term_of_uri "cic://Coq/Reals/Raxioms/INR.con")
+    Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
     end
   else 
     begin