X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommCheck.ml;h=e5629ccc8468b509b75c3fdb3254c21486185cbf;hp=93d1d03162f09db324668c9dbb34cad206ef3b94;hb=dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0;hpb=baa54e5db0fb93c4242dd1b67a5018ca63206cf6

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
index 93d1d0316..e5629ccc8 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
@@ -76,7 +76,7 @@ let rec recomm srcs st =
     if middle st then Printf.eprintf "middle: %S\n" s1;
     if !log_k then log prune (s1^s2);
     recomm tl @@ add hd @@ st
-  | ET.Title ss as hd :: tl        ->
+  | ET.Title ss :: tl              ->
     if middle st then Printf.eprintf "middle: TITLE\n";
     let b, ss1, ss2 = !c_line k_final false [] ss in
     let ss2 =
@@ -85,8 +85,8 @@ let rec recomm srcs st =
     let ss = List.rev_append ss1 ss2 in
     let s = String.concat " " ss in
     if !log_t then log blue s;
-    recomm tl @@ add hd @@ st
-  | ET.Slice ss as hd :: tl        ->
+    recomm tl @@ add (ET.Title ss) @@ st
+  | ET.Slice ss :: tl              ->
     if middle st then Printf.eprintf "middle: Section\n";
     let b, ss1, ss2 = !s_line k_final false [] ss in
     let ss2 =
@@ -95,7 +95,7 @@ let rec recomm srcs st =
     let ss = List.rev_append ss1 ss2 in
     let s = String.capitalize_ascii (String.concat " " ss) in
     if !log_s then log sky s;
-    recomm tl @@ add hd @@ st
+    recomm tl @@ add (ET.Slice ss) @@ st
   | ET.Other (_, s, _) as hd :: tl ->
     if !log_o && not (Array.mem s mute_o) then log black s;
     recomm tl @@ add hd @@ st