X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=95f40da5368ff06fe99991f33dc372c3d67f6d57;hb=32d3f10c1904d450ce8ea3525230acc6980a5601;hp=4dcf01c53b1a43f2793cf29ca374e456cbdba62c;hpb=7bc72d8afaebb1d2070a26b07f9bf4242b648e2c;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 4dcf01c53..95f40da53 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -95,3 +95,52 @@ let mk_appl he args =
   | NCic.Appl l -> NCic.Appl (l@args)
   | _ -> NCic.Appl (he::args)
 ;;
+
+let map_obj_kind f =
+ function
+    NCic.Constant (relev,name,bo,ty,attrs) ->
+     NCic.Constant (relev,name,HExtlib.map_option f bo, f ty,attrs)
+  | NCic.Fixpoint (ind,fl,attrs) ->
+     let fl =
+      List.map
+       (function (relevance,name,recno,ty,bo) -> relevance,name,recno,f ty,f bo)
+       fl
+     in
+      NCic.Fixpoint (ind,fl,attrs)
+  | NCic.Inductive (is_ind,lno,itl,attrs) ->
+      let itl = 
+        List.map
+         (fun (relevance,name,ty,cl) ->
+           let cl = 
+             List.map (fun (relevance, name, ty) ->
+                relevance, name, f ty)
+             cl
+           in
+           relevance, name, f ty, cl)
+         itl
+      in
+      NCic.Inductive (is_ind,lno,itl,attrs)
+;;
+
+let apply_subst subst t = 
+ let rec apply_subst subst () =
+ function
+    NCic.Meta (i,lc) ->
+     (try
+       let _,_,t,_ = NCicUtils.lookup_subst i subst in
+       let t = NCicSubstitution.subst_meta lc t in
+        apply_subst subst () t
+      with
+       Not_found ->
+        match lc with
+           _,NCic.Irl _ -> NCic.Meta (i,lc)
+         | n,NCic.Ctx l ->
+            NCic.Meta
+             (i,(0,NCic.Ctx
+                 (List.map (fun t ->
+                   apply_subst subst () (NCicSubstitution.lift n t)) l))))
+  | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
+ in
+  apply_subst subst () t
+;;
+