From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 31 Jul 2007 10:39:53 +0000 (+0000)
Subject: default equality stuff filtered out from hint rewrite
X-Git-Tag: make_still_working~6115
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eb12cc5c306d3b3eb18717ccca7e43504e3c3ba3;p=helm.git

default equality stuff filtered out from hint rewrite
---

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