diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-11 11:55:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-17 19:15:20 +0200 |
| commit | 94e8664074cfb987f8a63ca29c5436c861184b3a (patch) | |
| tree | ed520fdb1120c24fee4285e71ee73448d7d20c56 /tactics/equality.mli | |
| parent | 6d770156669dd9868ae7623b8f4302866e2cc8c7 (diff) | |
Stopping injection not to work on discriminable atoms (see #4890).
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index d979c580a..b47be3bbc 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -96,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic +(* Tells if tactic "discriminate" is applicable *) val discriminable : env -> evar_map -> constr -> constr -> bool + +(* Tells if tactic "injection" is applicable *) val injectable : env -> evar_map -> constr -> constr -> bool (* Subst *) |