tclCASE use result instead of adhoc type

Author: SkySkimmer

dev/ci/user-overlays/22013-SkySkimmer-logic_simpl.sh

@@ -0,0 +1 @@
+overlay tactician https://github.com/SkySkimmer/coq-tactician logic_simpl 22013

engine/profile_tactic.ml

@@ -379,8 +379,8 @@ let rec tclWRAPFINALLY before tac finally =
   let open Proofview in
   let open Proofview.Notations in
   before >>= fun v -> tclCASE tac >>= function
-  | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
-  | Next (ret, tac') -> tclOR
+  | Error (e, info) -> finally v >>= fun () -> tclZERO ~info e
+  | Ok (ret, tac') -> tclOR
                           (finally v >>= fun () -> tclUNIT ret)
                           (fun e -> tclWRAPFINALLY before (tac' e) finally)
 

engine/proofview.ml

@@ -341,15 +341,8 @@ let tclEXACTLY_ONCE e t =
 
 
 (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
-type 'a case =
-| Fail of Exninfo.iexn
-| Next of 'a * (Exninfo.iexn -> 'a tactic)
-let tclCASE t =
-  let map = function
-  | Error e -> Fail e
-  | Ok (x, t) -> Next (x, t)
-  in
-  Proof.map map (Proof.split t)
+type 'a case = ('a * (Exninfo.iexn -> 'a tactic), Exninfo.iexn) result
+let tclCASE = Proof.split
 
 let tclBREAK = Proof.break
 

engine/proofview.mli

@@ -229,9 +229,7 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
 (** [tclCASE t] splits [t] into its first success and a
     continuation. It is the most general primitive to control
     backtracking. *)
-type 'a case =
-  | Fail of Exninfo.iexn
-  | Next of 'a * (Exninfo.iexn -> 'a tactic)
+type 'a case = ('a * (Exninfo.iexn -> 'a tactic), Exninfo.iexn) result
 val tclCASE : 'a tactic -> 'a case tactic
 
 (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of

plugins/ltac2/tac2core.ml

@@ -1022,10 +1022,10 @@ let () =
 let () =
   define "case" (thunk valexpr @-> tac (result (pair valexpr (fun1 exn valexpr)))) @@ fun f ->
   Proofview.tclCASE (thaw f) >>= begin function
-  | Proofview.Next (x, k) ->
+  | Ok (x, k) ->
     let k (e,info) = set_bt info >>= fun info -> k (e,info) in
     return (Ok (x, k))
-  | Proofview.Fail e -> return (Error e)
+  | Error _ as e -> return e
   end
 
 let () =

tactics/class_tactics.ml

@@ -606,7 +606,7 @@ module Search = struct
             str " of status " ++ pr_goal_status status)
         in
         let rec kont = function
-          | Fail ((NonStuckFailure | StuckGoal as exn), info) when allow_out_of_order ->
+          | Error ((NonStuckFailure | StuckGoal as exn), info) when allow_out_of_order ->
             let () = ppdebug 1 (fun () ->
                 str "Goal " ++ int glid ++
                 str" is stuck or failed without being stuck, trying other tactics.")
@@ -619,13 +619,13 @@ module Search = struct
             in
             cycle 1 (* Puts the first goal last *) <*>
             fixpoint progress tacs ((glid, ev, status, tac) :: stuck) fk (* Launches the search on the rest of the goals *)
-          | Fail ie ->
+          | Error ie ->
             let () = ppdebug 1 (fun () ->
                 str "Goal " ++ int glid ++ str" has no more solutions, returning exception: "
                 ++ pr_internal_exception ie)
             in
             fk ie
-          | Next (res, fk') ->
+          | Ok (res, fk') ->
             let () = ppdebug 1 (fun () ->
                 str "Goal " ++ int glid ++ str" has a success, continuing resolution")
             in