X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=6aad3676d11176fa045cc26ebfed4df9190b92cb;hb=de4483296d06aac3df4da10d5401b1f97c4350ab;hp=712e8aae2d46b7e95ddf1520cc9b41e011b223e5;hpb=51971de8dfcf257680cf38f01f9bf53d9912a498;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index 712e8aae2..6aad3676d 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,11 +25,13 @@
 
 open Printf;;
 
+type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
+
 (* the list of known coercions (MUST be transitively closed) *)
 let coercions = ref [
   (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
    UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
-   UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ;
+   UriManager.uri_of_string "cic:/Coq/Reals/Raxioms/INR.con") ;
 
    (
      UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",