~pattern:
(None,[name,Cic.Implicit (Some `Hole)], None)
(ProofEngineTypes.const_lazy_term typ);
- ProofEngineStructuralRules.clear dummy
+ ProofEngineStructuralRules.clear [dummy]
]),
Some pat,gty
| _::_ -> assert false
selected_terms_with_context ([],[]) in
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
let uri,metasenv,pbo,pty = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
assert (hyps_pat = []); (*CSC: not implemented yet *)
+ let eq_URI =
+ match LibraryObjects.eq_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
+ in
let context_len = List.length context in
let subst,metasenv,u,_,selected_terms_with_context =
ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
~start:(
P.cut_tac
(C.Appl [
- (C.MutInd (LibraryObjects.eq_URI (), 0, [])) ;
+ (C.MutInd (eq_URI, 0, [])) ;
ty_of_with_what ;
what ;
with_what]))
(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