| 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 = []);
- uri,height,metasenv,subst,
+ refresh_uri uri,height,metasenv,subst,
NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
;;
let register tag require =
assert (not (List.mem tag !already_registered));
already_registered := tag :: !already_registered;
+ let old_require1 = !require1 in
require1 :=
- (fun (tag',data) as x ->
- if tag=tag' then
- require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
- else
- !require1 x);
+ (fun (tag',data) as x ->
+ if tag=tag' then
+ require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
+ else
+ old_require1 x);
(fun x -> tag,Obj.repr x)
let serialize = serialize