Procedural: we corrected two errors about the handling of mutcase (the "cases"

[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..f8ee5f1e5e929ab197773adaf6c8be5a567c0f3e 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 
@@ -319,3 +325,26 @@ let analyse_indty status ty =
 ;;
 
 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)
+;;