- (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in
- match Indexing.subsumption env table goal_equation with
- | Some (subst, (_,p,_,m)) ->
- let p = Inference.apply_subst subst (Inference.build_proof_term p) in
- let newp =
- let rec repl = function
- | Inference.ProofGoalBlock (_, gp) ->
- Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
- | Inference.NoProof -> Inference.BasicProof ([],p)
- | Inference.BasicProof _ -> Inference.BasicProof ([],p)
- | Inference.SubProof (t, i, p2) ->
- Inference.SubProof (t, i, repl p2)
- | _ -> assert false
- in
- repl proof
- in
- Some (newp,Inference.apply_subst_metasenv subst m @ menv)
- | None -> None)
+ (let goal_equation =
+ Equality.mk_equality
+ (0,(Equality.Exact (Cic.Rel (-1)),proof),(eq_ty,left,right,Eq),menv)
+ in
+ match Indexing.subsumption env table goal_equation with
+ | Some (subst, equality ) ->
+ let (_,(np,p),(ty,l,r,_),m,id) =
+ Equality.open_equality equality in
+ let p = Equality.apply_subst subst
+ (Equality.build_proof_term_old p) in
+ let newp =
+ let rec repl = function
+ | Equality.ProofGoalBlock (_, gp) ->
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,p), gp)
+ | Equality.NoProof ->
+ Equality.BasicProof (Equality.empty_subst,p)
+ | Equality.BasicProof _ ->
+ Equality.BasicProof (Equality.empty_subst,p)
+ | Equality.SubProof (t, i, p2) ->
+ Equality.SubProof (t, i, repl p2)
+ | _ -> assert false
+ in
+ repl proof
+ in
+ let newcicp,np,subst,cicmenv =
+ cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv)
+ in
+ Some
+ ((newcicp,np,subst,cicmenv),
+ (newp, Equality.apply_subst_metasenv subst m @ menv ))
+ | None -> None)