Avoid translating back recursive fixes to the same URI.

diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index 70d174e60c84ce3ba4b274b39f679b91cea1fb68..3f735a8249f0f23a098d41e18e951e907d351426 100644 (file)
--- 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,