From f7c55014aabb0d607449868e2522515db0b40568 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 1 May 2019 17:00:55 +0200
Subject: Make the check flag of conversion functions mandatory.

The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
---
 user-contrib/Ltac2/tac2tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'user-contrib')

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