- hExtlib: added debugging information for split_nth

[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 86487e20d5cc575dc054ef92b4fad67482e865d1..29eee6b7bf09da98310c0049ea98f1c71f18b05d 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 
@@ -314,8 +320,14 @@ 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)
 ;;
 
 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
+  status, (name, ctx, NCicUntrusted.apply_subst subst t)
+;;