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
let lit = Subst.apply_subst subst lit in
extract status 0 [] lit in
(* composition of all subst acting on goal *)
- let res_subst =
- let rec rsaux ongoal acc =
- function
- | [] -> acc (* is the final subst for refl *)
- | id::tl when ongoal ->
- let lit,vl,proof = get_literal id in
- (match proof with
- | Terms.Exact _ -> rsaux ongoal acc tl
- | Terms.Step (_, _, _, _, _, s) ->
- rsaux ongoal (s@acc) tl)
- | id::tl ->
- (* subst is the the substitution for refl *)
- rsaux (id=mp) subst tl
- in
- let r = rsaux false [] steps in
- (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
- prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
- r
+ let res_subst = subst
in
let rec aux ongoal seen = function
| [] -> NCic.Rel 1