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..faa0499049 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_prim3 "tac_unify" constr constr (option ident) begin fun x y db -> + Tac2tactics.unify x y db +end |