let text = skipped_txt ^ nonskipped_txt in
let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
let enriched_history_fragment =
- MatitaEngine.eval_ast ~do_heavy_checks:true
+ MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
+ "matita.do_heavy_checks")
lexicon_status grafite_status (text,prefix_len,st)
in
let enriched_history_fragment = List.rev enriched_history_fragment in
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