From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 1 Jun 2007 15:05:06 +0000 (+0000)
Subject: removed some refinement_toolkit
X-Git-Tag: make_still_working~6260
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e53dfd3fa17a77ab1fdd249ed2e5b6d0f9d94d88;p=helm.git

removed some refinement_toolkit
---

diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index fe1c961fb..42a19bcf9 100644
--- 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 789e7d00d..5dc086ec4 100644
--- 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 e621a7a0c..8ecabbbb6 100644
--- 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 a009944f8..1f4c1d12b 100644
--- 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 d0bdb4410..8750ce0f7 100644
--- 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 4307e6b03..d63e8805c 100644
--- 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 :