aboutsummaryrefslogtreecommitdiff
path: root/plugins/interface/paths.ml
diff options
context:
space:
mode:
authorglondu2009-12-02 08:36:14 +0000
committerglondu2009-12-02 08:36:14 +0000
commit3cb4411089c18351d57685f9abe455d3f61f308f (patch)
treec23e0d757eee079722f4fcc92b37e69c4ff4ef81 /plugins/interface/paths.ml
parent3e253de6854b139a8a1be76af2388ffa9a3dcdb2 (diff)
Remove interface plugin
It has moved to the contribs (Sophia-Antipolis/Interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/paths.ml')
-rw-r--r--plugins/interface/paths.ml26
1 files changed, 0 insertions, 26 deletions
diff --git a/plugins/interface/paths.ml b/plugins/interface/paths.ml
deleted file mode 100644
index dcccc39e83..0000000000
--- a/plugins/interface/paths.ml
+++ /dev/null
@@ -1,26 +0,0 @@
-let int_list_to_string s l =
- List.fold_left
- (fun s -> (fun v -> s ^ " " ^ (string_of_int v)))
- s
- l;;
-
-(* Given two paths, this function returns the longest common prefix and the
- two suffixes. *)
-let rec decompose_path
- : (int list * int list) -> (int list * int list * int list) =
- function
- (a::l,b::m) when a = b ->
- let (c,p1,p2) = decompose_path (l,m) in
- (a::c,p1,p2)
- | p1,p2 -> [], p1, p2;;
-
-let rec is_prefix p1 p2 = match p1,p2 with
- [], _ -> true
-| a::tl1, b::tl2 when a = b -> is_prefix tl1 tl2
-| _ -> false;;
-
-let rec lex_smaller p1 p2 = match p1,p2 with
- [], _ -> true
-| a::tl1, b::tl2 when a < b -> true
-| a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2
-| _ -> false;;