X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMisc.ml;h=53d1d1f67ec2440c2c3ce45df0958ab52b9edfd3;hb=caf822cbe34e204e6d1b72e272373b561c1a565a;hp=fe6fd35579cfa838a5f098fbd4b1fbc7a605a797;hpb=f3d0ba1e75bc3383d766f3a33a19352db19854df;p=helm.git diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml index fe6fd3557..53d1d1f67 100644 --- a/matita/matita/matitaMisc.ml +++ b/matita/matita/matitaMisc.ml @@ -38,8 +38,8 @@ let strip_suffix ~suffix s = let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file -let is_proof_script fname = true (** TODO Zack *) -let is_proof_object fname = true (** TODO Zack *) +let is_proof_script _fname = true (** TODO Zack *) +let is_proof_object _fname = true (** TODO Zack *) let append_phrase_sep s = if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then @@ -77,8 +77,8 @@ class shell_history size = let size = size + 1 in 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 "" + object + 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) @@ -149,8 +149,8 @@ let list_tl_at ?(equality=(==)) e l = let rec aux = function | [] -> raise Not_found - | hd :: tl as l when equality hd e -> l - | hd :: tl -> aux tl + | hd :: _ as l when equality hd e -> l + | _ :: tl -> aux tl in aux l