diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-05 18:13:23 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-05 20:50:24 +0100 |
| commit | c6d6e27330f0a1c9e89b6b60953d4df757edfdb8 (patch) | |
| tree | dccd305334c454e6834a019410429f51c7b6fba0 /tactics/equality.mli | |
| parent | 70e0d022333e0fc9e06b582f6831cbc698959cf0 (diff) | |
Exporting build_selector, a component of discriminate, for use in congruence.
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 |