X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FrolesEngine.ml;h=73cca4e6618da4ab5499a2cccbbedac16a3ae12b;hb=7666f9dddfcaca5671dd25d3cd2095481968c7bf;hp=4a3a92cb5b3ccc9e34cc2cadf324fc46813423d2;hpb=9bb0e91ff4c24ae6e51cac336b9edd6d6bf1ed0d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
index 4a3a92cb5..73cca4e66 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
@@ -67,6 +67,15 @@ let add_tops v =
   end;
   if ts <> [] then st.ET.t <- ts
 
+let rec add_matching () =
+  match EU.match_names 0 0 st.ET.t st.ET.w with
+  | None          -> ()
+  | Some  (ti,wi) ->
+    toggle_entry [1;ti];
+    toggle_entry [2;wi];
+    add_role ();
+    add_matching ()
+
 let read_waiting fname =
   if st.ET.s = [] then EU.raise_error ET.ENoStage else
   let ich = Scanf.Scanning.open_in fname in
@@ -90,3 +99,10 @@ let write_status () =
   let och = open_out fname in
   EO.out_status och st;
   close_out och
+
+let print_status () =
+  EO.out_status stdout st
+
+let visit_status before_t each_t after_t before_w each_w after_w =
+  EU.list_visit before_t each_t after_t EU.string_of_obj [1] st.ET.t;
+  EU.list_visit before_w each_w after_w EU.string_of_name [2] st.ET.w