Merge pull request #429 from SkySkimmer/revertcast

Adapt to coq/coq#14773 (convert_concl has a ~cast argument)
mattam82 · Oct 9, 2021 · 922467e · 922467e
2 parents 44a805e + 5bfc779
commit 922467e
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/src/depelim.ml b/src/depelim.ml
@@ -120,7 +120,7 @@ let dependent_pattern ?(pattern_term=true) c =
   in
   let concllda, evd = List.fold_left mklambda (pf_concl gl, project gl) subst in
   let conclapp = applistc concllda (List.rev_map pi1 subst) in
-    convert_concl ~check:false conclapp DEFAULTcast)
+    convert_concl ~cast:false ~check:false conclapp DEFAULTcast)
 
 let annot_of_context ctx =
   Array.map_of_list Context.Rel.Declaration.get_annot (List.rev ctx)
@@ -248,7 +248,7 @@ let pattern_call ?(pattern_term=true) c =
   in
   let concllda = List.fold_left mklambda (pf_concl gl) subst in
   let conclapp = applistc concllda (List.rev_map pi1 subst) in
-    (convert_concl ~check:false conclapp DEFAULTcast))
+    (convert_concl ~cast:false ~check:false conclapp DEFAULTcast))
 
 let destPolyRef sigma c =
   let open GlobRef in

diff --git a/src/equations_common.ml b/src/equations_common.ml
@@ -558,7 +558,7 @@ let autounfold_heads db db' cl gl =
     if did then
       match cl with
       | Some hyp -> Proofview.V82.of_tactic (change_in_hyp ~check:true None (make_change_arg c') hyp) gl
-      | None -> Proofview.V82.of_tactic (convert_concl ~check:false c' DEFAULTcast) gl
+      | None -> Proofview.V82.of_tactic (convert_concl ~cast:false ~check:false c' DEFAULTcast) gl
     else tclFAIL 0 (str "Nothing to unfold") gl
 
 type hintdb_name = string

diff --git a/src/principles_proofs.ml b/src/principles_proofs.ml
@@ -87,7 +87,7 @@ let _rewrite_try_change tac =
           | Some _ -> Proofview.tclZERO (RewriteSucceeded concl')
           | None -> Proofview.tclUNIT ())))
     (function
-      | (RewriteSucceeded concl', _) -> convert_concl ~check:false concl' REVERTcast
+      | (RewriteSucceeded concl', _) -> convert_concl ~cast:true ~check:false concl' DEFAULTcast
       | (exn, info) -> Proofview.tclZERO ~info exn))
 
 let autorewrite_one b =
@@ -491,7 +491,7 @@ let aux_ind_fun info chop nested unfp unfids p =
           in
           Tacticals.New.tclTHENLIST
             [observe_new "letin" (letin_pat_tac true None (Name id) (sigma, elim) occs);
-             observe_new "convert concl" (convert_concl ~check:false newconcl DEFAULTcast);
+             observe_new "convert concl" (convert_concl ~cast:false ~check:false newconcl DEFAULTcast);
              observe_new "clear body" (clear_body [id]);
              aux chop unfs unfids s]
         | _ ->
@@ -898,7 +898,7 @@ let prove_unfolding_lemma info where_map f_cst funf_cst p unfp gl =
   let my_simpl = opacified (to82 (simpl_in_concl)) in
   let unfolds base base' =
     tclTHEN (autounfold_heads [base] [base'] None)
-    (to82 (Tactics.reduct_in_concl ~check:false ((Reductionops.clos_norm_flags CClosure.betazeta), DEFAULTcast)))
+    (to82 (Tactics.reduct_in_concl ~cast:false ~check:false ((Reductionops.clos_norm_flags CClosure.betazeta), DEFAULTcast)))
   in
   let solve_rec_eq subst gl =
     match kind (project gl) (pf_concl gl) with
@@ -1149,7 +1149,7 @@ let ind_elim_tac indid inds mutinds info ind_fun =
             tclONCE (Tactics.apply app <*> Tactics.simpl_in_concl <*> eauto ~depth:None)]
 
     | _, LetIn (_, b, _, t') ->
-       tclTHENLIST [Tactics.convert_concl ~check:false (subst1 b t') DEFAULTcast;
+       tclTHENLIST [Tactics.convert_concl ~cast:false ~check:false (subst1 b t') DEFAULTcast;
                     applyind (pred leninds) (b :: args)]
     | _, Prod (_, _, t') ->
         tclTHENLIST [Tactics.intro;