let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let ty_set = Constr.constants_of ty in
let hyp_set = signature_of_hypothesis context metasenv in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let ty_set = Constr.constants_of ty in
let hyp_set = signature_of_hypothesis context metasenv in
let set_for_sigmatch =
Constr.UriManagerSet.remove u all_constants_closed in
if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
(* equality has a special treatment *)
let set_for_sigmatch =
Constr.UriManagerSet.remove u all_constants_closed in
if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
(* equality has a special treatment *)
let tfe =
Constr.SetSet.elements (types_for_equality metasenv goal)
in
List.fold_left
(fun acc l ->
let tyl = Constr.UriManagerSet.elements l in
let tfe =
Constr.SetSet.elements (types_for_equality metasenv goal)
in
List.fold_left
(fun acc l ->
let tyl = Constr.UriManagerSet.elements l in
let uris =
sigmatch ~dbd ~facts:false ~where:`Statement
(Some (u,[]),set_for_sigmatch)
let uris =
sigmatch ~dbd ~facts:false ~where:`Statement
(Some (u,[]),set_for_sigmatch)
let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
((proof, goal) as status)
=
let (_, metasenv, _subst, _, _, _) = proof in
((proof, goal) as status)
=
let (_, metasenv, _subst, _, _, _) = proof in