From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 12 Apr 2006 21:18:44 +0000 (+0000)
Subject: added patch to allow agin "match sin ? = ?"
X-Git-Tag: make_still_working~7418
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=cee71cb1bf82a6462be0939ff26610ce766a9170;p=helm.git

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 6c4dedd08..4c40f9e14 100644
--- 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 *)