background!)
2. the "Bad name" error is now a "Bad name" warning
Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
let name = UriManager.name_of_uri uri in
if not(CicPp.check name ty) then
- MatitaLog.error ("Bad name: "^name);
+ MatitaLog.warn ("Bad name: " ^ name);
assert (metasenv = metasenv');
let goalno =
match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in
class console ~(buffer: GText.buffer) () =
object (self)
val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
- val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+ val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
val message_tag = buffer#create_tag []
val debug_tag = buffer#create_tag [ `FOREGROUND "#888888" ]
method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s