Merge PR coq#12227: Spring cleaning of the tactic compatibility layer

Reviewed-by: gares

dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh

@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then
+
+    equations_CI_REF="refiner-rm-v82"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi

plugins/btauto/refl_btauto.ml

@@ -164,14 +164,17 @@ module Btauto = struct
 
   let reify env t = lapp eval [|convert_env env; convert t|]
 
-  let print_counterexample p penv gl =
+  let print_counterexample p penv =
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
     let var = lapp witness [|p|] in
     let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
-    let redfun, _ = Redexpr.reduction_of_red_expr (Refiner.pf_env gl) Genredexpr.(CbvVm None) in
-    let _, var = redfun Refiner.(pf_env gl) Refiner.(project gl) var in
+    let redfun, _ = Redexpr.reduction_of_red_expr env Genredexpr.(CbvVm None) in
+    let _, var = redfun env sigma var in
     let var = EConstr.Unsafe.to_constr var in
-    let rec to_list l = match decomp_term (Tacmach.project gl) l with
+    let rec to_list l = match decomp_term sigma l with
     | App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
     | App (c, [|_; h; t|])
@@ -196,7 +199,6 @@ module Btauto = struct
         let assign = List.combine penv var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
-          let sigma, env = Tacmach.project gl, Tacmach.pf_env gl in
           let term = Printer.pr_constr_env env sigma key in
           term ++ spc () ++ str ":=" ++ spc () ++ b
         in
@@ -205,7 +207,8 @@ module Btauto = struct
         str "Not a tautology:" ++ spc () ++ l
       with e when CErrors.noncritical e -> (str "Not a tautology")
     in
-    Tacticals.tclFAIL 0 msg gl
+    Tacticals.New.tclFAIL 0 msg
+  end
 
   let try_unification env =
     Proofview.Goal.enter begin fun gl ->
@@ -216,7 +219,7 @@ module Btauto = struct
       match t with
       | App (c, [|typ; p; _|]) when c === eq ->
       (* should be an equality [@eq poly ?p (Cst false)] *)
-          let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
+          let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (print_counterexample p env) in
           tac
       | _ ->
           let msg = str "Btauto: Internal error" in

plugins/funind/functional_principles_proofs.ml

@@ -41,7 +41,10 @@ let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
 let finish_proof dynamic_infos g =
   observe_tac "finish" (Proofview.V82.of_tactic assumption) g
 
-let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
+let refine c =
+  Proofview.V82.of_tactic
+    (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c))
+
 let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
 

plugins/ssr/ssrbwd.ml

@@ -55,18 +55,18 @@ let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)
 let interp_nbargs ist gl rc =
   try
     let rc6 = mkRApp rc (mkRHoles 6) in
-    let sigma, t = interp_open_constr ist gl (rc6, None) in
+    let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc6, None) in
     let si = sig_it gl in
     let gl = re_sig si sigma in
-    6 + Ssrcommon.nbargs_open_constr gl t
+    6 + Ssrcommon.nbargs_open_constr (pf_env gl) t
   with _ -> 5
 
 let interp_view_nbimps ist gl rc =
   try
-    let sigma, t = interp_open_constr ist gl (rc, None) in
+    let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc, None) in
     let si = sig_it gl in
     let gl = re_sig si sigma in
-    let pl, c = splay_open_constr gl t in
+    let pl, c = splay_open_constr (pf_env gl) t in
     if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl))
   with _ -> 0
 
@@ -88,7 +88,7 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)
 let apply_rconstr ?ist t gl =
 (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
   let n = match ist, DAst.get t with
-    | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
+    | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs (pf_env gl) (project gl) (EConstr.mkVar id)
     | Some ist, _ -> interp_nbargs ist gl t
     | _ -> anomaly "apply_rconstr without ist and not RVar" in
   let mkRlemma i = mkRApp t (mkRHoles i) in
@@ -97,7 +97,7 @@ let apply_rconstr ?ist t gl =
     if i > n then
       errorstrm Pp.(str"Cannot apply lemma "++pf_pr_glob_constr gl t)
     else try pf_match gl (mkRlemma i) (OfType cl) with _ -> loop (i + 1) in
-  refine_with (loop 0) gl
+  Proofview.V82.of_tactic (refine_with (loop 0)) gl
 
 let mkRAppView ist gl rv gv =
   let nb_view_imps = interp_view_nbimps ist gl rv in
@@ -112,26 +112,28 @@ let refine_interp_apply_view dbl ist gl gv =
     interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
   let rec loop = function
   | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
-  | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
+  | h :: hs -> (try Proofview.V82.of_tactic (refine_with (snd (interp_with h))) gl with _ -> loop hs) in
   loop (pair dbl (Ssrview.AdaptorDb.get dbl) @
         if dbl = Ssrview.AdaptorDb.Equivalence
         then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward))
         else [])
 
 let apply_top_tac =
-  Tacticals.tclTHENLIST [
+  Proofview.Goal.enter begin fun _ ->
+  Tacticals.New.tclTHENLIST [
     introid top_id;
-    apply_rconstr (mkRVar top_id);
-    old_cleartac [SsrHyp(None,top_id)]
+    Proofview.V82.tactic (apply_rconstr (mkRVar top_id));
+    cleartac [SsrHyp(None,top_id)]
   ]
+  end
 
 let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl ->
  let _, clr = interp_hyps ist gl gclr in
  let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
  let ggenl, tclGENTAC =
    if gviews <> [] && ggenl <> [] then
      let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in
-     [], Tacticals.tclTHEN (genstac (ggenl,[]))
+     [], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[])))
    else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
  tclGENTAC (fun gl ->
   match gviews, ggenl with
@@ -148,9 +150,9 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
   | [], [agens] ->
     let clr', (sigma, lemma) = interp_agens ist gl agens in
     let gl = pf_merge_uc_of sigma gl in
-    Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl
+    Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr']) gl
   | _, _ ->
-     Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl
+    Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [apply_top_tac; cleartac clr]) gl) gl
 )
 
-let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac
+let apply_top_tac = apply_top_tac