From e9513dd8c017f69aca8619758bfbef120f484b3f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 16:45:16 +0000 Subject: [PATCH] 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!!!! --- helm/software/components/ng_kernel/oCic2NCic.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index e414cfa56..767634329 100644 --- 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 -- 2.39.2