added patch to allow agin "match sin ? = ?"

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 6c4dedd086f34c140656de930ce7ca1735b2152a..4c40f9e14588686c9f9d879ab1721658b432eff3 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -221,9 +221,15 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
-  (* XXX use a real CIC -> string pretty printer *)
   let pp_macro = 
-    TAPp.pp_macro ~term_pp:(ApplyTransformation.txt_of_cic_term max_int [] []) 
+    let f t = ProofEngineReduction.replace 
+      ~equality:(fun _ t -> match t with Cic.Meta _ -> true | _ -> false)
+      ~what:[()] ~with_what:[Cic.Implicit None] ~where:t
+    in
+    let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+    TAPp.pp_macro 
+      ~term_pp:(fun x -> 
+        ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x))
   in
   match mac with
   (* WHELP's stuff *)