matitacLib: bugfix in .moo generation

[helm.git] / helm / software / matita / applyTransformation.ml

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 2309d8fb04f310690d933145bce503fca8ad03e1..5ae773c49de1b72df40b60294b1137e7b55f4543 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -177,13 +177,13 @@ let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm =
    let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
    remove_closed_substs s
 
-let enable_notations x = () (* function
+let enable_notations = function
    | true -> 
       CicNotation.set_active_notations
          (List.map fst (CicNotation.get_all_notations ()))
    | false ->
       CicNotation.set_active_notations []
-*)
+
 let txt_of_cic_object 
  ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas
  n style ?flavour prefix obj