]> matita.cs.unibo.it Git - helm.git/commitdiff
added patch to allow agin "match sin ? = ?"
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 12 Apr 2006 21:18:44 +0000 (21:18 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 12 Apr 2006 21:18:44 +0000 (21:18 +0000)
helm/software/matita/matitaScript.ml

index 6c4dedd086f34c140656de930ce7ca1735b2152a..4c40f9e14588686c9f9d879ab1721658b432eff3 100644 (file)
@@ -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 *)