From cee71cb1bf82a6462be0939ff26610ce766a9170 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Apr 2006 21:18:44 +0000 Subject: [PATCH] added patch to allow agin "match sin ? = ?" --- helm/software/matita/matitaScript.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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 *) -- 2.39.2