X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FrolesUtils.ml;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FrolesUtils.ml;h=7c779fddfebdcf6aadcad2d331c158eba49e0acc;hb=f07cd97493f650ee779be874d1159c0e807f8273;hp=dcf7addef89f3c139cbfa6f47ddc531e198c362b;hpb=9bb0e91ff4c24ae6e51cac336b9edd6d6bf1ed0d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
index dcf7addef..7c779fddf 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
@@ -149,6 +149,16 @@ let rec get_tops v = function
     end else
       ds, ts
 
+let rec match_names oi ni os ns =
+  match os, ns with
+  | _         , []        -> None
+  | []        , _         -> None
+  | (_,o)::otl,(_,n)::ntl ->
+    let b = compare_names (snd o) n in
+    if b > 0 then match_names oi (succ ni) os ntl else
+    if b < 0 then match_names (succ oi) ni otl ns else
+    Some (oi, ni)
+
 let new_status = {
   ET.r = []; ET.s = []; ET.t = []; ET.w = [];
 }