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

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 1deb935d5c..4e0866a0c5 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1299,7 +1299,7 @@ let ssrpatterntac _ist arg gl =
   let concl_x = EConstr.of_constr concl_x in
   let gl, tty = pf_type_of gl t in
   let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in
-  Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
+  Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl
 
 (* Register "ssrpattern" tactic *)
 let () =
-- 
cgit v1.2.3