let module R = CicReduction in
let module S = CicSubstitution in
let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
hd::tl ->
(match hd with
contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
let generalize_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
terms ~status:((proof,goal) as status)
=
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv in
let typ =
match terms with
[] -> assert false
~start:
(P.cut_tac
(C.Prod(
- (mk_fresh_name_callback context C.Anonymous typ),
+ (mk_fresh_name_callback metasenv context C.Anonymous typ),
typ,
(ProofEngineReduction.replace_lifting_csc 1
~equality:(==)