in aux ft (List.rev pl)
;;
- (* we should better split forward and backward rewriting *)
let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
let module NCicBlob =
NCicBlob.NCicBlob(
let get_literal id =
let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
let lit =match lit with
- | Terms.Predicate t -> assert false
+ | Terms.Predicate t -> t (* assert false *)
| Terms.Equation (l,r,ty,_) ->
Terms.Node [ Terms.Leaf eqP(); ty; l; r]
in