From 32957dedce16e57467f94da83caf2617815028cd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 21 Feb 2008 19:02:04 +0000 Subject: [PATCH] Avoid translating back recursive fixes to the same URI. --- helm/software/components/ng_kernel/nCic2OCic.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index 70d174e60..3f735a824 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -34,7 +34,12 @@ let convert_term uri n_fl t = if NUri.eq u uri then Cic.Rel (n_fl - i + k) else - Cic.Const (NUri.ouri_of_nuri u,[]) + let ouri = NUri.ouri_of_nuri u in + let ouri = + UriManager.uri_of_string + (UriManager.buri_of_uri ouri ^ "/" ^ + UriManager.name_of_uri ouri ^ string_of_int i ^ ".con") in + Cic.Const (ouri,[]) | _ -> assert false in convert_term 0 t @@ -69,7 +74,8 @@ let convert_nobj = function | u,_,_,_,NCic.Fixpoint (is_fix, fl, _) -> List.map (fun nth -> - let name = UriManager.name_of_uri (NUri.ouri_of_nuri u) in + let name = + UriManager.name_of_uri (NUri.ouri_of_nuri u) ^ string_of_int nth in let buri = UriManager.buri_of_uri (NUri.ouri_of_nuri u) in let uri = UriManager.uri_of_string (buri ^"/"^name^".con") in uri, -- 2.39.2