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 f8ee5f1e5e929ab197773adaf6c8be5a567c0f3e..323b1e6fc0ee1b744f77c1405c73a26d5d7430bc 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -329,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)
 ;;