X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=6a38873fc360d9b238f3ff13bbed0174fc521bd7;hb=7cdfae2ec209750303818f2e39f31e4739286858;hp=5b4c9940cbd623c700c197b501d937a5a04ab5f3;hpb=246f3c2f2d26655129efacf830ecff47094795b4;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 5b4c9940c..6a38873fc 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -14,6 +14,9 @@
 module C = NCic
 module R = NReference
 
+let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);;
+let set_head_beta_reduce = (:=) head_beta_reduce;;
+
 let r2s pp_fix_name r = 
   try
     match r with
@@ -128,6 +131,14 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
       F.fprintf f "]@] @]";
    | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) -> 
        F.fprintf f "BAD APPLICATION"
+   | C.Appl (C.Meta (n,lc) :: args) when List.mem_assoc n subst -> 
+       let _,_,t,_ = List.assoc n subst in
+       let hd = NCicSubstitution.subst_meta lc t in
+       aux ctx 
+         (!head_beta_reduce ~upto:(List.length args)
+           (match hd with
+           | NCic.Appl l -> NCic.Appl (l@args)
+           | _ -> NCic.Appl (hd :: args)))
    | C.Appl l -> 
        F.fprintf f "@[<hov 2>";
        if not toplevel then F.fprintf f "(";