+let magic = 2;;
+
+let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
+
+let refresh_uri_in_universe =
+ List.map (fun (x,u) -> x, refresh_uri u)
+;;
+
+let rec refresh_uri_in_term =
+ function
+ | NCic.Const (NReference.Ref (u,spec)) ->
+ NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
+ | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l))
+ | NCic.Match (NReference.Ref (uri,spec),outtype,term,pl) ->
+ let r = NReference.reference_of_spec (refresh_uri uri) spec in
+ let outtype = refresh_uri_in_term outtype in
+ let term = refresh_uri_in_term term in
+ let pl = List.map refresh_uri_in_term pl in
+ NCic.Match (r,outtype,term,pl)
+ | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t
+;;
+
+let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) =
+ assert (metasenv = []);
+ assert (subst = []);
+ refresh_uri uri,height,metasenv,subst,
+ NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
+;;