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 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]))