Patch to add a debugging string to HExtlib.split_nth reverted

[helm.git] / helm / software / components / ng_tactics / nTacStatus.ml

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 55448ae2db03615416aec06118be58bacb492a58..323b1e6fc0ee1b744f77c1405c73a26d5d7430bc 100644 (file)
--- 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 
@@ -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)
 ;;