diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 88ce9868af..45a4799ea1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -257,7 +257,7 @@ let tclNOTSAMEGOAL tac = Proofview.Goal.goals >>= fun gls -> let check accu gl' = gl' >>= fun gl' -> - let accu = accu || Goal.V82.same_goal sigma ev (project gl') (goal gl') in + let accu = accu || Proofview.Progress.goal_equal sigma ev (project gl') (goal gl') in Proofview.tclUNIT accu in Proofview.Monad.List.fold_left check false gls >>= fun has_same -> @@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot = match EConstr.kind sigma hdcncl with | Ind (ind_sp,u) -> let pr1 = - lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) + lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) in begin match lft2rgt, cls with | Some true, None @@ -417,7 +417,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim -> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) - {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} + {elimindex = None; elimbody = (elim,NoBindings) } end let adjust_rewriting_direction args lft2rgt = @@ -446,7 +446,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in - match match_with_equality_type sigma t with + match match_with_equality_type env sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels) @@ -462,7 +462,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type sigma t' with + match match_with_equality_type env sigma t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c @@ -743,7 +743,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let hd2,args2 = whd_all_stack env sigma t2 in match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_) - when Int.equal (List.length args1) (constructor_nallargs_env env sp1) + when Int.equal (List.length args1) (constructor_nallargs env sp1) -> let sorts' = Sorts.List.intersect sorts (allowed_sorts env (fst sp1)) @@ -751,7 +751,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) if eq_constructor sp1 sp2 then - let nparams = inductive_nparams_env env ind1 in + let nparams = inductive_nparams env ind1 in let params1,rargs1 = List.chop nparams args1 in let _,rargs2 = List.chop nparams args2 in let (mib,mip) = lookup_mind_specif env ind1 in @@ -966,9 +966,10 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let gen_absurdity id = Proofview.Goal.enter begin fun gl -> + let env = pf_env gl in let sigma = project gl in let hyp_typ = pf_get_hyp_typ id gl in - if is_empty_type sigma hyp_typ + if is_empty_type env sigma hyp_typ then simplest_elim (mkVar id) else @@ -1066,7 +1067,7 @@ let onNegatedEquality with_evars tac = let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in match EConstr.kind sigma (hnf_constr env sigma ccl) with - | Prod (_,t,u) when is_empty_type sigma u -> + | Prod (_,t,u) when is_empty_type env sigma u -> tclTHEN introf (onLastHypId (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) @@ -1612,10 +1613,10 @@ let cutSubstInHyp l2r eqn id = tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENFIRST (tclTHENLIST [ - (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly)); + (change_in_hyp ~check:true None (make_change_arg typ) (id,InHypTypeOnly)); (replace_core (onHyp id) l2r eqn) ]) - (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))) + (change_in_hyp ~check:true None (make_change_arg expected) (id,InHypTypeOnly))) end let try_rewrite tac = |