diff options
| -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 6c3f465f33..237ec8b995 100644 --- a/user-contrib/Ltac2/Std.v +++ b/user-contrib/Ltac2/Std.v @@ -145,7 +145,7 @@ Ltac2 @ external set : evar_flag -> (unit -> ident option * constr) -> clause -> Ltac2 @ external remember : evar_flag -> ident option -> (unit -> constr) -> intro_pattern option -> clause -> unit := "ltac2" "tac_remember". Ltac2 @ external destruct : evar_flag -> induction_clause list -> - constr_with_bindings option -> unit := "ltac2" "tac_induction". + constr_with_bindings option -> unit := "ltac2" "tac_destruct". Ltac2 @ external induction : evar_flag -> induction_clause list -> constr_with_bindings option -> unit := "ltac2" "tac_induction". |