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.

8 files changed, 21 insertions, 21 deletions

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
 
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 99a9c1ab9a..355c16bfd0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1574,8 +1574,8 @@ let newfail n s =
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
   (* For compatibility *)
-  let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
-  let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
+  let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
+  let beta_hyp id = Tactics.reduct_in_hyp ~check:false Reductionops.nf_betaiota (id, InHyp) in
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 3f69701bd3..b02b97f656 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -89,10 +89,10 @@ let protect_red map env sigma c0 =
   EConstr.of_constr (eval 0 c)
 
 let protect_tac map =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) None
+  Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
+  Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))
 
 
 (****************************************************************************)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a4caeb403c..56f17703ff 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -427,7 +427,7 @@ let mk_anon_id t gl_ids =
   Id.of_string_soft (Bytes.to_string (loop (n - 1)))
 
 let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast
-let convert_concl t = Tactics.convert_concl t DEFAULTcast
+let convert_concl ~check t = Tactics.convert_concl ~check t DEFAULTcast
 
 let rename_hd_prod orig_name_ref gl =
   match EConstr.kind (project gl) (pf_concl gl) with
@@ -799,7 +799,7 @@ let discharge_hyp (id', (id, mode)) gl =
   | NamedDecl.LocalDef (_, v, t), _ ->
     let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in
      Proofview.V82.of_tactic
-       (convert_concl (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl
+       (convert_concl ~check:true (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl
 
 (* wildcard names *)
 let clear_wilds wilds gl =
@@ -1170,7 +1170,7 @@ let gentac gen gl =
   ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
   let gl = pf_merge_uc ucst gl in
   if conv
-  then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (old_cleartac clr) gl
+  then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl
   else genclrtac cl [c] clr gl
 
 let genstac (gens, clr) =
@@ -1215,7 +1215,7 @@ let unprotecttac gl =
   let prot, _ = EConstr.destConst (project gl) c in
   Tacticals.onClause (fun idopt ->
     let hyploc = Option.map (fun id -> id, InHyp) idopt in
-    Proofview.V82.of_tactic (Tactics.reduct_option 
+    Proofview.V82.of_tactic (Tactics.reduct_option ~check:false
       (Reductionops.clos_norm_flags 
         (CClosure.RedFlags.mkflags 
           [CClosure.RedFlags.fBETA;
@@ -1282,10 +1282,10 @@ let clr_of_wgen gen clrs = match gen with
   | clr, _ -> old_cleartac clr :: clrs
 
 
-let reduct_in_concl t = Tactics.reduct_in_concl (t, DEFAULTcast)
+let reduct_in_concl ~check t = Tactics.reduct_in_concl ~check (t, DEFAULTcast)
 let unfold cl =
   let module R = Reductionops in let module F = CClosure.RedFlags in
-  reduct_in_concl (R.clos_norm_flags (F.mkflags
+  reduct_in_concl ~check:false (R.clos_norm_flags (F.mkflags
     (List.map (fun c -> F.fCONST (fst (destConst (EConstr.Unsafe.to_constr c)))) cl @
        [F.fBETA; F.fMATCH; F.fFIX; F.fCOFIX])))
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 58ce84ecb3..575f016014 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -252,7 +252,7 @@ val ssrevaltac :
   Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tactic
 
 val convert_concl_no_check : EConstr.t -> unit Proofview.tactic
-val convert_concl : EConstr.t -> unit Proofview.tactic
+val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic
 
 val red_safe :
   Reductionops.reduction_function ->
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 =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 01d71aa96a..4d4400a0f8 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -56,7 +56,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
   | _ -> c, pfe_type_of gl c in
   let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in
-  Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl
+  Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl')) (introid id) gl
 
 open Util
 
@@ -161,7 +161,7 @@ let havetac ist
      let gl, ty = pfe_type_of gl t in
      let ctx, _ = EConstr.decompose_prod_n_assum (project gl) 1 ty in
      let assert_is_conv gl =
-       try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl
+       try Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.it_mkProd_or_LetIn concl ctx)) gl
        with _ -> errorstrm (str "Given proof term is not of type " ++
          pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in
      gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
@@ -471,7 +471,7 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
     if hint = nohint then
       Proofview.tclUNIT ()
     else
-      let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
+      let betaiota = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
       (* Usefulness of check_numgoals: tclDISPATCH would be enough,
          except for the error message w.r.t. the number of
          provided/expected tactics, as the last one is implied *)
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 () =