cic_unification removed

[helm.git] / matita / matita / matitaScript.ml

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 9fa039b311add2643ac4c3acde8d9d7bd1886a15..b6ec2a51f01262a58b483a093a7dafea26b4f7c1 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -224,14 +224,6 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
       [(grafite_status#set_proof_status No_proof), parsed_text ],"", 
         parsed_text_length *)
-  | TA.Inline (_, suri, params) ->
-       let str = "\n\n" ^ 
-         ApplyTransformation.txt_of_inline_macro
-          ~map_unicode_to_tex:(Helm_registry.get_bool
-            "matita.paste_unicode_as_tex")
-          params suri 
-       in
-       [], str, String.length parsed_text
                                 
 and eval_executable include_paths (buffer : GText.buffer) guistuff
 grafite_status user_goal unparsed_text skipped_txt nonskipped_txt