From 3ca9529b5fdbb8e2a3dc18e38862cbe351e8e0e0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Jun 2019 17:03:29 +0200
Subject: Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same
 thing.

The ML wrapper was wrongly calling induction instead of destruct.
---
 user-contrib/Ltac2/Std.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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".
-- 
cgit v1.2.3