X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_extraction%2Fcoq.ml;h=130f7ebdfc10c3c818a6939d5a71e2a1f0a24257;hb=f34f2623a3133e235331d0c0c1830ec213dd09f1;hp=f68562c2037ee23072d29082c1c129b266af8144;hpb=7e6fea0332e132a8cb89c689ba68c5e884c4354c;p=helm.git

diff --git a/matita/components/ng_extraction/coq.ml b/matita/components/ng_extraction/coq.ml
index f68562c20..130f7ebdf 100644
--- a/matita/components/ng_extraction/coq.ml
+++ b/matita/components/ng_extraction/coq.ml
@@ -25,7 +25,7 @@ let cut_ident skip_quote s =
         numpart (n-1) n'
       else if code_of_0 <= c && c <= code_of_9 then
         numpart (n-1) (n-1)
-      else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
+      else if skip_quote && (c = Char.code '\'' || c = Char.code '_') then
         numpart (n-1) (n-1)
       else
         n'
@@ -34,9 +34,9 @@ let cut_ident skip_quote s =
 
 let forget_subscript id =
   let numstart = cut_ident false id in
-  let newid = String.make (numstart+1) '0' in
+  let newid = Bytes.make (numstart+1) '0' in
   String.blit id 0 newid 0 numstart;
-  newid
+  Bytes.to_string newid
 
 (* Namegen.ml *)
 
@@ -58,18 +58,18 @@ let lift_subscript id =
         add (carrypos-1)
       end
       else begin
-        let newid = String.copy id in
-        String.fill newid (carrypos+1) (len-1-carrypos) '0';
+        let newid = Bytes.of_string id in
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
         newid.[carrypos] <- Char.chr (Char.code c + 1);
-        newid
+        Bytes.to_string newid
       end
     else begin
-      let newid = id^"0" in
+      let newid = Bytes.of_string (id^"0") in
       if carrypos < len-1 then begin
-        String.fill newid (carrypos+1) (len-1-carrypos) '0';
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
         newid.[carrypos+1] <- '1'
       end;
-      newid
+      Bytes.to_string newid
     end
   in add (len-1)