diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index d7e697aed..91c577405 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -42,7 +42,7 @@ open Ind_tables open Eqschemes open Locus open Locusops -open Misctypes +open Tactypes open Proofview.Notations open Unification open Context.Named.Declaration @@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'} + Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = @@ -546,6 +546,12 @@ let apply_special_clear_request clear_flag f = e when catchable_exception e -> tclIDTAC end +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + let general_multi_rewrite with_evars l cl tac = let do1 l2r f = Proofview.Goal.enter begin fun gl -> @@ -1037,7 +1043,7 @@ let onEquality with_evars tac (c,lbindc) = let t = type_of c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in - let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in + let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in tclTHEN |