From 56bf133e9df9c7b689e0c3059fffdc1f8736a936 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Feb 2005 13:42:35 +0000 Subject: [PATCH] fix in the coercions list generation and aded a function to know the known coercions --- helm/ocaml/cic_unification/coercGraph.ml | 5 +++-- helm/ocaml/cic_unification/coercGraph.mli | 4 ++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index e256a19b8..eb1dc44ae 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -188,11 +188,12 @@ let close_coercion_graph src tgt uri = ((src,tgt,c_uri),(c_uri,named_obj,u)) ) todo_list) in - coercions := !coercions @ new_coercions; + coercions := !coercions @ new_coercions @ [src,tgt,uri]; new_coercions_obj ;; - +let get_coercions_list () = + !coercions (* stupid case *) diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli index 3c03312c7..9cbff65b9 100644 --- a/helm/ocaml/cic_unification/coercGraph.mli +++ b/helm/ocaml/cic_unification/coercGraph.mli @@ -29,3 +29,7 @@ val look_for_coercion : val close_coercion_graph: UriManager.uri -> UriManager.uri -> UriManager.uri -> (UriManager.uri * Cic.obj * CicUniv.universe_graph) list + +val get_coercions_list: + unit -> (UriManager.uri * UriManager.uri * UriManager.uri) list + -- 2.39.2