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/ssr/ssrequality.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/ssr/ssrequality.ml')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ad20113320..e349031952 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -118,7 +118,7 @@ let newssrcongrtac arg ist gl =
     match try Some (pf_unify_HO gl_c (pf_concl gl) c)
           with exn when CErrors.noncritical exn -> None with
     | Some gl_c ->
-        tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c)))
+        tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true (fs gl_c c)))
           (t_ok (proj gl_c)) gl
     | None -> t_fail () gl in 
   let mk_evar gl ty = 
@@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl =
     try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) 
     with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in
   let _ = conclude () in
-  Proofview.V82.of_tactic (convert_concl concl) gl
+  Proofview.V82.of_tactic (convert_concl ~check:true concl) gl
 ;;
 
 let foldtac occ rdx ft gl = 
@@ -303,7 +303,7 @@ let foldtac occ rdx ft gl =
   let concl0 = EConstr.Unsafe.to_constr concl0 in
   let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in
   let _ = conclude () in
-  Proofview.V82.of_tactic (convert_concl (EConstr.of_constr concl)) gl
+  Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.of_constr concl)) gl
 ;;
 
 let converse_dir = function L2R -> R2L | R2L -> L2R
@@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
           let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
           let gl = pf_merge_uc_of sigma gl in
-          Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl
+          Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl
     else
       let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
       let r3, _, r3t  = 
@@ -644,7 +644,7 @@ let unfoldtac occ ko t kt gl =
   let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in
   let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in
   Proofview.V82.of_tactic
-    (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
+    (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
 
 let unlocktac ist args gl =
   let utac (occ, gt) gl =
-- 
cgit v1.2.3