From ace0d12b876bf15a1eed28f04118b9984e33b570 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Aug 2012 08:02:28 +0000 Subject: [PATCH] Name mangling until separate extraction is implemented. --- matita/components/ng_kernel/nCicExtraction.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 72bb35b08..ac6848b83 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -676,7 +676,15 @@ type 'a result = ;; let fresh_name_of_ref status ref = - let candidate = NCicPp.r2s status true ref in + (*CSC: Patch while we wait for separate compilation *) + let candidate = + let name = NCicPp.r2s status true ref in + let NReference.Ref (uri,_) = ref in + let path = NUri.baseuri_of_uri uri in + let path = String.sub path 5 (String.length path - 5) in + let path = Str.global_replace (Str.regexp "/") "_" path in + path ^ "_" ^ name + in let rec freshen candidate = if GlobalNames.mem candidate (snd status#extraction_db) then freshen (candidate ^ "'") -- 2.39.2