X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FrolesEngine.ml;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Froles%2FrolesEngine.ml;h=285807169f05696a37ab673f422c5cdc0f985358;hb=f07cd97493f650ee779be874d1159c0e807f8273;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..285807169 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,6 @@ 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