From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Aug 2012 08:02:28 +0000 (+0000)
Subject: Name mangling until separate extraction is implemented.
X-Git-Tag: make_still_working~1514
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ace0d12b876bf15a1eed28f04118b9984e33b570

Name mangling until separate extraction is implemented.
---

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 ^ "'")