update in binaries for λδ

[helm.git] / matita / matita / contribs / lambdadelta / bin / roles / rolesUtils.ml

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
index dcf7addef89f3c139cbfa6f47ddc531e198c362b..7c779fddfebdcf6aadcad2d331c158eba49e0acc 100644 (file)
--- 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 = [];
 }