diff options
Diffstat (limited to 'user-contrib/Ltac2/Std.v')
| -rw-r--r-- | user-contrib/Ltac2/Std.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v index 17741e563d..3675df9f75 100644 --- a/user-contrib/Ltac2/Std.v +++ b/user-contrib/Ltac2/Std.v @@ -260,4 +260,4 @@ Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) l Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto". -Ltac2 @ external unify : constr -> constr -> ident option -> unit := "ltac2" "tac_unify". +Ltac2 @ external unify : constr -> constr -> unit := "ltac2" "tac_unify". |