X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMisc.ml;h=e612b88031396548b92cbc5f1ae69579d7da14b9;hb=f34f2623a3133e235331d0c0c1830ec213dd09f1;hp=fe6fd35579cfa838a5f098fbd4b1fbc7a605a797;hpb=7e6fea0332e132a8cb89c689ba68c5e884c4354c;p=helm.git diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml index fe6fd3557..e612b8803 100644 --- a/matita/matita/matitaMisc.ml +++ b/matita/matita/matitaMisc.ml @@ -78,7 +78,7 @@ class shell_history size = let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in let incr x = (x + 1) mod size in object (self) - val data = Array.create size "" + val data = Array.make size "" inherit basic_history (0, -1 , -1) @@ -106,7 +106,7 @@ class shell_history size = class ['a] browser_history ?memento size init = object (self) initializer match memento with Some m -> self#load m | _ -> () - val data = Array.create size init + val data = Array.make size init inherit basic_history (0, 0, 0)