diff options
| author | Pierre-Marie Pédrot | 2020-04-28 15:45:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-29 09:41:04 +0200 |
| commit | 23952efb51664ef30fee44bff31dcbf38c5bff63 (patch) | |
| tree | 2cd76a7983ad121e32a786155af54ecd7c145364 /tactics/equality.ml | |
| parent | 6a6272ad2b452624e75418245fbbf30d3dc5597f (diff) | |
Merge the call to tclEFFECTS into find_scheme.
This encapsulates better the invariants of this function.
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 8f2336c0e0..f3073acb0a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -411,8 +411,7 @@ let find_elim hdcncl lft2rgt dep cls ot = match EConstr.kind sigma hdcncl with | Ind (ind,u) -> - let c, eff = find_scheme scheme_name ind in - Proofview.tclEFFECTS eff <*> + find_scheme scheme_name ind >>= fun c -> pf_constr_of_global (GlobRef.ConstRef c) | _ -> assert false end @@ -1001,14 +1000,13 @@ let ind_scheme_of_eq lbeq to_kind = let from_kind = inductive_sort_family mip in (* use ind rather than case by compatibility *) let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in - let c, eff = find_scheme kind (destIndRef lbeq.eq) in - GlobRef.ConstRef c, eff + find_scheme kind (destIndRef lbeq.eq) >>= fun c -> + Proofview.tclUNIT (GlobRef.ConstRef c) let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = build_coq_I () >>= fun i -> - let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in - Proofview.tclEFFECTS eff <*> + ind_scheme_of_eq lbeq to_kind >>= fun eq_elim -> pf_constr_of_global eq_elim >>= fun eq_elim -> Proofview.tclUNIT (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) @@ -1352,10 +1350,10 @@ let inject_if_homogenous_dependent_pair ty = check_required_library ["Coq";"Logic";"Eqdep_dec"]; let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in - let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in + find_scheme (!eq_dec_scheme_kind_name()) ind >>= fun c -> (* cut with the good equality and prove the requested goal *) tclTHENLIST - [Proofview.tclEFFECTS eff; + [ intro; onLastHyp (fun hyp -> Tacticals.New.pf_constr_of_global Coqlib.(lib_ref "core.eq.type") >>= fun ceq -> |