let clearbody ~hyp =
let clearbody (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,_,_ = CicUtil.lookup_meta goal metasenv in
let string_of_name =
function
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
PET.mk_tactic clearbody
let clear_one ~hyp =
let clear_one (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty =
CicUtil.lookup_meta goal metasenv
in
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
PET.mk_tactic clear_one
try List.combine froms tos
with Invalid_argument _ -> raise (PET.Fail (lazy error))
in
- let curi, metasenv, pbo, pty, attrs = proof in
+ let curi, metasenv, _subst, pbo, pty, attrs = proof in
let metano, _, _ = CicUtil.lookup_meta goal metasenv in
let rename_map = function
| Some (Cic.Name hyp, decl_or_def) as entry ->
| conjecture -> conjecture
in
let metasenv = List.map map metasenv in
- (curi, metasenv, pbo, pty, attrs), [goal]
+ (curi, metasenv, _subst, pbo, pty, attrs), [goal]
in
PET.mk_tactic rename