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

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 70854e6e3c..0857c05968 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -514,7 +514,7 @@ let autounfold_one db cl =
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (make_change_arg c') hyp
+      | Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
       | None -> convert_concl ~check:false c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
-- 
cgit v1.2.3