diff options
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 *) |