Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
;;
-(* adds a symmetry step *)
-let symmetric pred eq eq_ty l id uri m =
- let pred =
- Cic.Lambda (Cic.Name "Sym",eq_ty,
- Cic.Appl [CicSubstitution.lift 1 eq ;
- CicSubstitution.lift 1 eq_ty;
- Cic.Rel 1;CicSubstitution.lift 1 l])
- in
- let prefl =
- Equality.Exact (Cic.Appl
- [Cic.MutConstruct(uri,0,1,[]);eq_ty;l])
- in
- let id1 =
- let eq = Equality.mk_equality (0,prefl,(eq_ty,l,l,Eq),m) in
- let (_,_,_,_,id) = Equality.open_equality eq in
- id
- in
- Equality.Step(Subst.empty_subst,
- (Equality.Demodulation,id1,(Utils.Left,id),pred))
-;;
-
let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
(*
let names = names_of_context ctx in
Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
*)
match ty with
- | Cic.Appl[Cic.MutInd(uri,_,_) as eq;eq_ty;left;right]
+ | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
(let goal_equation =
Equality.mk_equality
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
let p =
if pos = Utils.Left then
- symmetric pred eq eq_ty l id uri m
+ Equality.symmetric eq_ty l id uri m
else
p
in