diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2stdlib.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2stdlib.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml index 895b6d3975..c7dfb3e69e 100644 --- a/user-contrib/Ltac2/tac2stdlib.ml +++ b/user-contrib/Ltac2/tac2stdlib.ml @@ -572,3 +572,7 @@ end let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs -> Tac2tactics.typeclasses_eauto str n dbs end + +let () = define_prim2 "tac_unify" constr constr begin fun x y -> + Tac2tactics.unify x y +end |