X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=29eee6b7bf09da98310c0049ea98f1c71f18b05d;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=55448ae2db03615416aec06118be58bacb492a58;hpb=8d7287519cc51145fcac0ee603ba136dc749857d;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 55448ae2d..29eee6b7b 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -99,6 +99,12 @@ let term_of_cic_term s t c =
   s, t
 ;;
 
+let ppterm status t =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let _,context,t = t in
+  NCicPp.ppterm ~metasenv ~subst ~context t
+;;
+
 let disambiguate status t ty context =
  let status, expty = 
    match ty with 
@@ -314,7 +320,7 @@ let analyse_indty status ty =
  let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in
  let _,_,_,cl = List.nth tl i in
  let consno = List.length cl in
- let left, right = HExtlib.split_nth lno args in
+ let left, right = HExtlib.split_nth "NTS 1" lno args in
  status, (ref, consno, left, right)
 ;;
 
@@ -323,22 +329,5 @@ let mk_cic_term c t = None,c,t ;;
 let apply_subst status ctx t =
  let status, (name,_,t) = relocate status ctx t in
  let _,_,_,subst,_ = status.pstatus in
- let rec aux ctx =
-  function
-     NCic.Meta (i,lc) ->
-      (try
-        let _,_,t,_ = NCicUtils.lookup_subst i subst in
-        let t = NCicSubstitution.subst_meta lc t in
-         aux ctx 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 -> aux ctx (NCicSubstitution.lift n t)) l))))
-   | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx aux t
- in
-  status, (name, ctx, aux ctx t)
+  status, (name, ctx, NCicUntrusted.apply_subst subst t)
 ;;