added tentative elim

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 5b4c9940cbd623c700c197b501d937a5a04ab5f3..6a38873fc360d9b238f3ff13bbed0174fc521bd7 100644 (file)
--- 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 "(";