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.
---
 plugins/funind/recdef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3c2b03dfe0..3dd3a430e8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -701,7 +701,7 @@ let mkDestructEq :
         let changefun patvars env sigma =
           pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
         in
-	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
+        Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
-- 
cgit v1.2.3