+ if !usedb then
+ begin
+ MQueryGenerator.init () ;
+ CicTextualParser0.set_locate_object
+ (function id ->
+ let MathQL.MQRefs uris = MQueryGenerator.locate id in
+ let uri =
+ match uris with
+ [] -> None
+ | [uri] -> Some uri
+ | _ -> None (* here we must let the user choose one uri *)
+ in
+ match uri with
+ Some uri' ->
+ if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+ Some (Cic.Const (UriManager.uri_of_string uri',0))
+ else
+ let uri'',typeno =
+(*CSC: the locate query now looks only for inductive type blocks ;-( *)
+(*CSC: when it will be correctly implemented we will have to work *)
+(*CSC: here on the fragment identifier *)
+ uri',0
+ in
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+ Some (Cic.MutInd (UriManager.uri_of_string uri'',0,typeno))
+ | None -> None
+ )
+ end ;