From eb12cc5c306d3b3eb18717ccca7e43504e3c3ba3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 Jul 2007 10:39:53 +0000 Subject: [PATCH] default equality stuff filtered out from hint rewrite --- helm/software/matita/matitaScript.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index a007e7023..c29e15533 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -488,6 +488,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let proof_status = proof,user_goal' in if rewrite then let l = MQ.equations_for_goal ~dbd proof_status in + let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length -- 2.39.2