diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2tactics.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2tactics.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli index f63f7e722a..47a3fd5987 100644 --- a/user-contrib/Ltac2/tac2tactics.mli +++ b/user-contrib/Ltac2/tac2tactics.mli @@ -119,6 +119,8 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list -> val typeclasses_eauto : Class_tactics.search_strategy option -> int option -> Id.t list option -> unit Proofview.tactic +val unify : constr -> constr -> unit tactic + val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic val contradiction : constr_with_bindings option -> unit tactic |