Incredible, but true! Our name mangling clashed with one identifier in the

library of Coq, generating two functions that mutually called each other,
making the type-checker diverge!!!!

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index e414cfa56dc4061d32c2485ed1a1105d709b91ac..767634329b0ff8971559b79f060758129aa3fad3 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -203,7 +203,8 @@ let convert_term uri t =
         let buri = 
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
-            UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con")
+            UriManager.name_of_uri uri ^ "___" ^
+             string_of_int (List.length ctx)^".con")
         in
         let bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
@@ -241,7 +242,8 @@ let convert_term uri t =
         let buri = 
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
-            UriManager.name_of_uri uri ^ string_of_int (List.length ctx)^".con")
+            UriManager.name_of_uri uri ^ "___" ^
+             string_of_int (List.length ctx)^".con")
         in
         let bad_bctx, fixpoints_tys, tys, _ = 
           List.fold_right