Bug fixed: name in letin was printed as "previous" even if given.

[helm.git] / helm / software / components / library / cicCoercion.ml

diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index fe1c961fb3c8dd7791250ee97e783b56fa30584f..42a19bcf92fcea3cbcab72129101c62ea0a87b27 100644 (file)
--- a/helm/software/components/library/cicCoercion.ml
+++ b/helm/software/components/library/cicCoercion.ml
@@ -26,8 +26,7 @@
 (* $Id$ *)
 
 let close_coercion_graph_ref = ref
- (fun _ _ _ _ _ -> [] : 
-   RefinementTool.kit -> 
+ (fun _ _ _ _ -> [] : 
    CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
    string (* baseuri *) ->
      (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
@@ -35,6 +34,6 @@ let close_coercion_graph_ref = ref
 
 let set_close_coercion_graph f = close_coercion_graph_ref := f;;
 
-let close_coercion_graph r c1 c2 u s = 
-  !close_coercion_graph_ref r c1 c2 u s
+let close_coercion_graph c1 c2 u s = 
+  !close_coercion_graph_ref c1 c2 u s
 ;;