diff options
| author | Pierre-Marie Pédrot | 2019-06-16 17:03:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-16 17:03:29 +0200 |
| commit | 3ca9529b5fdbb8e2a3dc18e38862cbe351e8e0e0 (patch) | |
| tree | 975eb71258f604af95a525522d29cfe856789391 | |
| parent | 5d58496c27fc5767c7841734c0f01a739cf529ab (diff) | |
Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.
The ML wrapper was wrongly calling induction instead of destruct.
| -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". |