From e53dfd3fa17a77ab1fdd249ed2e5b6d0f9d94d88 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Jun 2007 15:05:06 +0000 Subject: [PATCH] removed some refinement_toolkit --- helm/software/components/library/cicCoercion.ml | 7 +++---- helm/software/components/library/cicCoercion.mli | 4 +--- helm/software/components/library/librarySync.ml | 2 +- helm/software/components/tactics/closeCoercionGraph.ml | 2 +- helm/software/components/tactics/closeCoercionGraph.mli | 1 - helm/software/components/tactics/tactics.mli | 2 +- 6 files changed, 7 insertions(+), 11 deletions(-) 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 : -- 2.39.2