diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cList.ml | 2 | ||||
| -rw-r--r-- | lib/errors.ml | 14 | ||||
| -rw-r--r-- | lib/flags.ml | 8 | ||||
| -rw-r--r-- | lib/genarg.ml | 6 | ||||
| -rw-r--r-- | lib/iArray.ml | 2 | ||||
| -rw-r--r-- | lib/iStream.ml | 2 | ||||
| -rw-r--r-- | lib/int.ml | 3 | ||||
| -rw-r--r-- | lib/serialize.ml | 13 | ||||
| -rw-r--r-- | lib/trie.ml | 2 |
9 files changed, 5 insertions, 47 deletions
diff --git a/lib/cList.ml b/lib/cList.ml index 385c80b62..36dad3235 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -306,8 +306,6 @@ let subtract cmp l1 l2 = let unionq l1 l2 = union (==) l1 l2 let subtractq l1 l2 = subtract (==) l1 l2 -let tabulate = init - let interval n m = let rec interval_n (l,m) = if n > m then l else interval_n (m::l, pred m) diff --git a/lib/errors.ml b/lib/errors.ml index 9b2e9370d..9df276465 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -19,17 +19,9 @@ exception Anomaly of string option * std_ppcmds (* System errors *) let make_anomaly ?label pp = Anomaly (label, pp) -let anomaly_gen label pp = - raise (Anomaly (label, pp)) - -let anomaly ?loc ?label pp = - match loc with +let anomaly ?loc ?label pp = match loc with | None -> raise (Anomaly (label, pp)) - | Some loc -> - Loc.raise loc (Anomaly (label, pp)) - -let anomalylabstrm string pps = - anomaly_gen (Some string) pps + | Some loc -> Loc.raise loc (Anomaly (label, pp)) let is_anomaly = function | Anomaly _ -> true @@ -106,8 +98,6 @@ let print e = isn't printed (used in Ltac debugging). *) let print_no_report e = print_gen (print_anomaly false) !handle_stack e -let print_anomaly e = print_anomaly true e - (** Predefined handlers **) let _ = register_handler begin function diff --git a/lib/flags.ml b/lib/flags.ml index 91e28132a..3118901ac 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -179,14 +179,6 @@ let is_standard_doc_url url = url = Coq_config.wwwrefman || url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) -(* same as in System, but copied here because of dependencies *) -let canonical_path_name p = - let current = Sys.getcwd () in - Sys.chdir p; - let result = Sys.getcwd () in - Sys.chdir current; - result - (* Options for changing coqlib *) let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" diff --git a/lib/genarg.ml b/lib/genarg.ml index 306cdbed8..89b6f23de 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -154,10 +154,6 @@ let has_type (t, v) u = argument_type_eq t u let unquote x = x -type an_arg_of_this_type = Obj.t - -let in_generic t x = (t, Obj.repr x) - type ('a,'b) abstract_argument_type = argument_type type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type @@ -237,7 +233,7 @@ struct (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) - let rec obj t = match t with + let obj t = match t with | ExtraArgType s -> Obj.magic (get_obj0 s) | _ -> assert false diff --git a/lib/iArray.ml b/lib/iArray.ml index 8dbe3f6c6..3cbee45b6 100644 --- a/lib/iArray.ml +++ b/lib/iArray.ml @@ -452,8 +452,6 @@ struct let get = M.get -let set = M.set - let of_array (t : 'a array) : 'a M.t = let tag = Obj.tag (Obj.repr t) in let () = if tag = Obj.double_array_tag then diff --git a/lib/iStream.ml b/lib/iStream.ml index 065155f08..da54d9f7b 100644 --- a/lib/iStream.ml +++ b/lib/iStream.ml @@ -26,7 +26,7 @@ let rec force s = match Lazy.force s with let force s = force s; s -let rec is_empty s = match Lazy.force s with +let is_empty s = match Lazy.force s with | Nil -> true | Cons (_, _) -> false diff --git a/lib/int.ml b/lib/int.ml index 43d6d037d..1403dc510 100644 --- a/lib/int.ml +++ b/lib/int.ml @@ -49,7 +49,6 @@ module List = struct end let min (i : int) j = if i < j then i else j -let max (i : int) j = if i > j then i else j (** Utility function *) let rec next from upto = @@ -83,7 +82,7 @@ struct let reroot t = rerootk t (fun () -> ()) - let rec get t i = + let get t i = let () = assert (0 <= i) in match !t with | Root a -> diff --git a/lib/serialize.ml b/lib/serialize.ml index 92dcca2c5..386ab8e45 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -25,10 +25,6 @@ exception Marshal_error (** Utility functions *) -let rec has_flag (f : string) = function - | [] -> false - | (k, _) :: l -> CString.equal k f || has_flag f l - let rec get_attr attr = function | [] -> raise Not_found | (k, v) :: l when CString.equal k attr -> v @@ -186,13 +182,6 @@ let to_state_id xml = let of_edit_or_state_id = function | Interface.Edit id -> ["object","edit"], of_edit_id id | Interface.State id -> ["object","state"], of_state_id id -let to_edit_or_state_id attrs xml = - try - let obj = get_attr "object" attrs in - if obj = "edit"then Interface.Edit (to_edit_id xml) - else if obj = "state" then Interface.State (to_state_id xml) - else raise Marshal_error - with Not_found -> raise Marshal_error let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) @@ -410,7 +399,6 @@ module ReifType : sig (* {{{ *) type value_type val erase : 'a val_t -> value_type val print_type : value_type -> string - val same_type : 'a val_t -> value_type -> bool val document_type_encoding : (xml -> string) -> unit @@ -432,7 +420,6 @@ end = struct type 'a val_t = value_type let erase (x : 'a val_t) : value_type = x - let same_type (x : 'a val_t) (y : value_type) = Pervasives.compare (erase x) y = 0 let unit_t = Unit let string_t = String diff --git a/lib/trie.ml b/lib/trie.ml index a4a348c19..7efce9785 100644 --- a/lib/trie.ml +++ b/lib/trie.ml @@ -52,8 +52,6 @@ let labels (Node (_,m)) = (** FIXME: this is order-dependent. Try to find a more robust presentation? *) List.rev (T_codom.fold (fun x _ acc -> x::acc) m []) -let in_dom (Node (_,m)) lbl = T_codom.mem lbl m - let is_empty_node (Node(a,b)) = (X.is_nil a) && (T_codom.is_empty b) let assure_arc m lbl = |