match t with
| Terms.Leaf _
| Terms.Var _ ->
- let module NCicBlob = NCicBlob.NCicBlob(
- struct
- let metasenv = [] let subst = [] let context = []
- end)
- in
+ let module NCicBlob = NCicBlob.NCicBlob in
let module Pp = Pp.Pp(NCicBlob) in
prerr_endline ("term: " ^ Pp.pp_foterm ft);
prerr_endline ("path: " ^ String.concat ","
let mk_proof status ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps=
let module NCicBlob =
- NCicBlob.NCicBlob(
- struct
- let metasenv = [] let subst = [] let context = []
- end)
+ NCicBlob.NCicBlob
in
let module Pp = Pp.Pp(NCicBlob)
in