X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=33276cc3df689942cd19391af7e2c30d92647d1c;hb=5450fa91891df49587fedff6edd6179cf1bbc879;hp=8664add9b99955cafda1661117f46f80e4c2d559;hpb=a71920f51fcaecbe19812e255231e545fe013cfc;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 8664add9b..33276cc3d 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -26,6 +26,12 @@ let rec refresh_uri_in_term =
   | 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
 ;;
 
@@ -194,12 +200,13 @@ module Serializer(S: sig type status end) =
   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