aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/tac2tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib/Ltac2/tac2tactics.ml')
-rw-r--r--user-contrib/Ltac2/tac2tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 603e00c815..a8c1a67f6f 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -167,7 +167,7 @@ let change pat c cl =
delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma
in
let cl = mk_clause cl in
- Tactics.change pat c cl
+ Tactics.change ~check:true pat c cl
end
let rewrite ev rw cl by =