diff options
| author | Pierre-Marie Pédrot | 2017-09-05 00:35:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 00:36:04 +0200 |
| commit | ebe95a28cf012aff33eb5ce167be6520e6643cfd (patch) | |
| tree | 7899394e30ae4097936d4d4477c1f1ca48192466 /theories | |
| parent | ada4c3aadb5c6b1870c2bf962ef9e1b07cc4bb05 (diff) | |
More static invariants for typeclass_eauto.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Std.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Std.v b/theories/Std.v index b667258aa2..5201fa819d 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -226,4 +226,4 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto". -Ltac2 @ external typeclasses_eauto : bool -> strategy -> int option -> ident list -> unit := "ltac2" "tac_typeclasses_eauto". +Ltac2 @ external typeclasses_eauto : strategy -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto". |