X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.ml;h=cefb46e29d1bea322b50d66216cffde1b5c519c5;hb=47a9eb47d4215450230840bc66570ce412d0ce79;hp=b145c157acf979449bf1d815b2d68cc992139189;hpb=907f919aba0f21b18acff8a8e1c266ab92d10baf;p=helm.git diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index b145c157a..cefb46e29 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -82,14 +82,8 @@ let _ = sequents_viewer#load_logo; cic_math_view#set_href_callback (Some (fun uri -> - let uri = - try - `Uri (UriManager.uri_of_string uri) - with - UriManager.IllFormedUri _ -> - `NRef (NReference.reference_of_string uri) - in - (MatitaMathView.cicBrowser ())#load uri)); + let uri = `NRef (NReference.reference_of_string uri) in + (MatitaMathView.cicBrowser ())#load uri)); let browser_observer _ = MatitaMathView.refresh_all_browsers () in let sequents_observer grafite_status = sequents_viewer#reset; @@ -163,7 +157,7 @@ let _ = (fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug := mi#active; MultiPassDisambiguator.debug := mi#active; NCicMetaSubst.debug := mi#active); addDebugCheckbox "reduction logging" - (fun mi () -> NCicReduction.debug := mi#active; CicReduction.ndebug := mi#active); + (fun mi () -> NCicReduction.debug := mi#active); addDebugSeparator (); addDebugItem "Expand virtuals" (fun _ -> (MatitaScript.current ())#expandAllVirtuals);