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
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 "(";