diff options
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 1122615c3..47cb6b82f 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -79,6 +79,8 @@ val injClause : intro_patterns option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic val injHyp : clear_flag -> Id.t -> unit Proofview.tactic val injConcl : unit Proofview.tactic +val simpleInjClause : evars_flag -> + constr with_bindings destruction_arg option -> unit Proofview.tactic val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic |