removed some refinement_toolkit

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
 ;;

diff --git a/helm/software/components/library/cicCoercion.mli b/helm/software/components/library/cicCoercion.mli
index 789e7d00dff19a512230e84975f0b94c67b640b0..5dc086ec44cf2a9668355f550a8a430be3390715 100644 (file)
--- a/helm/software/components/library/cicCoercion.mli
+++ b/helm/software/components/library/cicCoercion.mli
@@ -26,14 +26,12 @@
 (* This module implements the Coercions transitive closure *)
 
 val set_close_coercion_graph : 
-  (RefinementTool.kit -> 
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+  (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
   string (* baseuri *) ->
     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
   -> unit
 
 val close_coercion_graph:
-  RefinementTool.kit -> 
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
   string (* baseuri *) ->
     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index e621a7a0cf1311ef26319e7363714db36fce5383..8ecabbbb6aeb435b44c735d744d709f37b97007a 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -282,7 +282,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
     (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
     let new_coercions = 
-      CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+      CicCoercion.close_coercion_graph src_carr tgt_carr uri 
        baseuri
     in
     let new_coercions = 

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index a009944f8c26fe4b14caf41059507e0022e72ddf..1f4c1d12b2182055ddf994bcfb9110475ac25e4e 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -313,7 +313,7 @@ let number_if_already_defined buri name l =
 (* given a new coercion uri from src to tgt returns 
  * a list of (new coercion uri, coercion obj, universe graph) 
  *)
-let close_coercion_graph _ src tgt uri baseuri =
+let close_coercion_graph src tgt uri baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
   let todo_list = get_closure_coercions src tgt uri coercions in

diff --git a/helm/software/components/tactics/closeCoercionGraph.mli b/helm/software/components/tactics/closeCoercionGraph.mli
index d0bdb44107efa5069aaaa2fba6b90c74d88ef672..8750ce0f7888f2bb359b5624aef88404d58bb376 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.mli
+++ b/helm/software/components/tactics/closeCoercionGraph.mli
@@ -26,7 +26,6 @@
 (* This module implements the Coercions transitive closure *)
 
 val close_coercion_graph:
-  RefinementTool.kit -> 
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
   string (* baseuri *) ->
     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 4307e6b034f4f82729ecda83cccd93e8c4e23a90..d63e8805cf6d846e92b63d16e4c74cd236c9a9ce 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun  1 13:27:04 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun  1 17:03:59 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :