let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
match t with
Cic.MutInd (uri,_,_)
| Cic.MutConstruct (uri,_,_,_) ->
match t with
Cic.MutInd (uri,_,_)
| Cic.MutConstruct (uri,_,_,_) ->
Cic.InductiveDefinition(tl,_,_,_) ->
snd
(List.fold_left
Cic.InductiveDefinition(tl,_,_,_) ->
snd
(List.fold_left
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 only constants uri =
prerr_endline (UriManager.string_of_uri uri);
let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
let only constants uri =
prerr_endline (UriManager.string_of_uri uri);
let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
let newty = types_of_equality ty in
(i+1,Constr.SetSet.union newty acc))
(1,all) context
let newty = types_of_equality ty in
(i+1,Constr.SetSet.union newty acc))
(1,all) context
let ty_set = Constr.constants_of ty in
let hyp_set = signature_of_hypothesis context metasenv in
let set = Constr.UriManagerSet.union ty_set hyp_set in
let ty_set = Constr.constants_of ty in
let hyp_set = signature_of_hypothesis context metasenv in
let set = Constr.UriManagerSet.union ty_set hyp_set 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