X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=6d1797677a6f23b8c587afe71709990f9e4189b1;hb=db7f6d6b32515c091e0f338dd4903624f35f27ac;hp=43b4a78a3c59428bc7f5b2ef094c2a4de45065be;hpb=2338b758114eb40daf3fadf4fb016a9a1af541b6;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 43b4a78a3..6d1797677 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -26,13 +26,19 @@ 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
 ;;
 
 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
 ;;