Bug fixed: propagation of left expected parameters is now working correctly also

[helm.git] / matita / components / content_pres / termContentPres.ml

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index ae447476042d7ea5af675a8fa975f3701d2b4682..6b0d9d0c8595c4ade106306369efb9acc20e9389 100644 (file)
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -524,8 +524,7 @@ let add_pretty_printer status l2 (CicNotationParser.CL1P (l1,precedence)) =
        level1_patterns21 =
         IntMap.add id l1' status#content_pres_db.level1_patterns21;
        pattern21_matrix = (l2',id)::status#content_pres_db.pattern21_matrix } in
-  let status = load_patterns21 status status#content_pres_db.pattern21_matrix in
-   status,id
+  load_patterns21 status status#content_pres_db.pattern21_matrix 
 
   (* presentation -> content *)