From: Ferruccio Guidi Date: Wed, 23 Nov 2016 20:14:11 +0000 (+0000) Subject: a linearized reference was still present ... X-Git-Tag: make_still_working~528 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fc577e43ddbfce9a9c049cbc1ffdf97f8da57fce;p=helm.git a linearized reference was still present ... --- diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 09441303b..ea9683e18 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -333,7 +333,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) HExtlib.safe_remove filename in object (self) - val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec"; + val mutable gviz_uri = + let uri = NUri.uri_of_string "cic:/dummy/dec.con" in + NReference.reference_of_spec uri NReference.Decl; val dep_contextual_menu = GMenu.menu ()