~pattern:
(None,[name,Cic.Implicit (Some `Hole)], None)
(ProofEngineTypes.const_lazy_term typ);
- ProofEngineStructuralRules.clear dummy
+ ProofEngineStructuralRules.clear [dummy]
]),
Some pat,gty
| _::_ -> assert false
let t1 = CicMetaSubst.apply_subst subst t1 in
let t2 = CicMetaSubst.apply_subst subst t2 in
let ty = CicMetaSubst.apply_subst subst ty in
+ let pbo = CicMetaSubst.apply_subst subst pbo in
+ let pty = CicMetaSubst.apply_subst subst pty in
let equality = CicMetaSubst.apply_subst subst equality in
let abstr_gty =
ProofEngineReduction.replace_lifting_csc 0
(function ((proof,goal) as status) ->
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let hyp =
+ let hyps =
try
match List.hd context with
- Some (Cic.Name name,_) -> name
+ Some (Cic.Name name,_) -> [name]
| _ -> assert false
with (Failure "hd") -> assert false
in
ProofEngineTypes.apply_tactic
- (ProofEngineStructuralRules.clear ~hyp) status))
+ (ProofEngineStructuralRules.clear ~hyps) status))
~continuation:(aux_tac (n + 1) tl));
T.id_tac])
status