diff options
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index f84dafb31..458d8f372 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -117,3 +117,8 @@ val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic val replace_term : bool option -> constr -> clause -> unit Proofview.tactic val set_eq_dec_scheme_kind : mutual scheme_kind -> unit + +(* [build_selector env sigma i c t u v] matches on [c] of + type [t] and returns [u] in branch [i] and [v] on other branches *) +val build_selector : env -> evar_map -> int -> constr -> types -> + constr -> constr -> constr |