Remove the deprecated functions from refiner, moving them to Tacticals.

4 files changed, 226 insertions, 359 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 705a1a62ce..d65c2f0de9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1103,8 +1103,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
   | TacShowHyps tac ->
          Proofview.V82.tactic begin
-           tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
-         end [@ocaml.warning "-3"]
+           Tacticals.tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
+         end
   | TacAbstract (t,ido) ->
       let call = LtacMLCall tac in
       let trace = push_trace(None,call) ist in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 874bab277d..3c6a5d1694 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -8,15 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Pp
-open CErrors
 open Util
 open Evd
 
 type tactic = Proofview.V82.tac
 
-module NamedDecl = Context.Named.Declaration
-
 let sig_it x = x.it
 let project x = x.sigma
 
@@ -27,235 +23,11 @@ let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig
 
 let refiner = Logic.refiner
 
-(*********************)
-(*   Tacticals       *)
-(*********************)
-
-
-let unpackage glsig = (ref (glsig.sigma)), glsig.it
-
-let repackage r v = {it = v; sigma = !r; }
-
-let apply_sig_tac r tac g =
-  Control.check_for_interrupt (); (* Breakpoint *)
-  let glsigma = tac (repackage r g) in
-  r := glsigma.sigma;
-  glsigma.it
-
-(* [goal_goal_list : goal sigma -> goal list sigma] *)
-let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; }
-
-(* identity tactic without any message *)
-let tclIDTAC gls = goal_goal_list gls
-
-(* the message printing identity tactic *)
-let tclIDTAC_MESSAGE s gls =
-  Feedback.msg_info (hov 0 s); tclIDTAC gls
-
-(* General failure tactic *)
-let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s)
-
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
-(* The Fail tactic *)
-let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
-
-let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
-
-let start_tac gls =
-  let sigr, g = unpackage gls in
-  (sigr, [g])
-
-let finish_tac (sigr,gl) = repackage sigr gl
-
-(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last
-   m subgoals, and [tac] on the others *)
-let thens3parts_tac tacfi tac tacli (sigr,gs) =
-  let nf = Array.length tacfi in
-  let nl = Array.length tacli in
-  let ng = List.length gs in
-  if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals.");
-  let gll =
-      (List.map_i (fun i ->
-        apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
-        0 gs) in
-    (sigr,List.flatten gll)
-
-(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
-let thensf_tac taci tac = thens3parts_tac taci tac [||]
-
-(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
-let thensi_tac tac (sigr,gs) =
-  let gll =
-    List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
-  (sigr, List.flatten gll)
-
-let then_tac tac = thensf_tac [||] tac
-
-(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
-   applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
-   the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
-   subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
-   error if the number of resulting subgoals is strictly less than [n+m] *)
-let tclTHENS3PARTS tac1 tacfi tac tacli gls =
-  finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls)))
-
-(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
-   to [gls] and applies [t1], ..., [tn] to the first [n] resulting
-   subgoals, and [tac2] to the others subgoals. Raises an error if
-   the number of resulting subgoals is strictly less than [n] *)
-let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||]
-
-(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
-   to [gls] and applies [t1], ..., [tn] to the last [n] resulting
-   subgoals, and [tac2] to the other subgoals. Raises an error if the
-   number of resulting subgoals is strictly less than [n] *)
-let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
-
-(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
-   [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
-   number of subgoals is *)
-let tclTHEN_i tac taci gls =
-  finish_tac (thensi_tac taci (then_tac tac (start_tac gls)))
-
-(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
-   [tac2] to every resulting subgoals *)
-let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
-
-(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
-   [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
-   an error if the number of resulting subgoals is not [n] *)
-let tclTHENSV tac1 tac2v =
-  tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||]
-
-let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
-
-(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
-   to the last resulting subgoal *)
-let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
-
-(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
-   to the first resulting subgoal *)
-let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
-
-(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
-   convenient than [tclTHEN] when [n] is large. *)
-let rec tclTHENLIST = function
-    [] -> tclIDTAC
-  | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
-
-(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
-let tclMAP tacfun l =
-  List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
-
-(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
-the goal unchanged *)
-let tclPROGRESS tac ptree =
-  let rslt = tac ptree in
-  if Goal.V82.progress rslt ptree then rslt
-  else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
-
-(* Execute tac, show the names of new hypothesis names created by tac
-   in the "as" format and then forget everything. From the logical
-   point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
-   except that it takes the time and memory of tac and prints "as"
-   information). The resulting (unchanged) goals are printed *after*
-   the as-expression, which forces pg to some gymnastic.
-   TODO: Have something similar (better?) in the xml protocol.
-   NOTE: some tactics delete hypothesis and reuse names (induction,
-   destruct), this is not detected by this tactical. *)
-let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
-    : Goal.goal list Evd.sigma =
-  let oldhyps = pf_hyps goal in
-  let rslt:Goal.goal list Evd.sigma = tac goal in
-  let { it = gls; sigma = sigma; } = rslt in
-  let hyps =
-    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
-  let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in
-  let newhyps =
-    List.map
-      (fun hypl -> List.subtract cmp hypl oldhyps)
-      hyps
-  in
-  let s =
-    let frst = ref true in
-    List.fold_left
-    (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
-      ^ (List.fold_left
-           (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc)
-           "" lh))
-    "" newhyps in
-  Feedback.msg_notice
-    (str "<infoH>"
-      ++  (hov 0 (str s))
-      ++  (str "</infoH>"));
-  tclIDTAC goal;;
-
-
 let catch_failerror (e, info) =
   match e with
   | FailError (lvl,s) when lvl > 0 ->
     Exninfo.iraise (FailError (lvl - 1, s), info)
   | e -> Control.check_for_interrupt ()
-
-(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
-let tclORELSE0 t1 t2 g =
-  try
-    t1 g
-  with (* Breakpoint *)
-    | e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in catch_failerror e; t2 g
-
-(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
-   then applies t2 *)
-let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
-
-(* applies t1;t2then if t1 succeeds or t2else if t1 fails
-   t2* are called in terminal position (unless t1 produces more than
-   1 subgoal!) *)
-let tclORELSE_THEN t1 t2then t2else gls =
-  match
-    try Some(tclPROGRESS t1 gls)
-    with e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in catch_failerror e; None
-  with
-    | None -> t2else gls
-    | Some sgl ->
-        let sigr, gl = unpackage sgl in
-        finish_tac (then_tac t2then  (sigr,gl))
-
-(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
-let tclTRY f = (tclORELSE0 f tclIDTAC)
-
-let tclTHENTRY f g = (tclTHEN f (tclTRY g))
-
-(* Try the first tactic that does not fail in a list of tactics *)
-
-let rec tclFIRST = function
-  | [] -> tclFAIL_s "No applicable tactic."
-  |  t::rest -> tclORELSE0 t (tclFIRST rest)
-
-(* Fails if a tactic did not solve the goal *)
-let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
-
-(* Iteration tacticals *)
-
-let tclDO n t =
-  let rec dorec k =
-    if k < 0 then user_err ~hdr:"Refiner.tclDO"
-      (str"Wrong argument : Do needs a positive integer.");
-    if Int.equal k 0 then tclIDTAC
-    else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1)))
-  in
-  dorec n
-
-
-(* Beware: call by need of CAML, g is needed *)
-let rec tclREPEAT t g =
-  tclORELSE_THEN t (tclREPEAT t) tclIDTAC g
-
-let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
-
-(* Change evars *)
-let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index a3cbfb5d5d..0ea630fdbc 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -24,107 +24,9 @@ val pf_hyps : Goal.goal sigma -> named_context
 
 val refiner : check:bool -> Constr.t -> unit Proofview.tactic
 
-(** {6 Tacticals. } *)
-
-(** [tclIDTAC] is the identity tactic without message printing*)
-val tclIDTAC          : tactic
-[@@ocaml.deprecated "Use Tactical.New.tclIDTAC"]
-val tclIDTAC_MESSAGE  : Pp.t -> tactic
-[@@ocaml.deprecated]
-
-(** [tclEVARS sigma] changes the current evar map *)
-val tclEVARS : evar_map -> tactic
-[@@ocaml.deprecated "Use Proofview.Unsafe.tclEVARS"]
-
-
-(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
-   [tac2] to every resulting subgoals *)
-val tclTHEN          : tactic -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHEN"]
-
-(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
-   convenient than [tclTHEN] when [n] is large *)
-val tclTHENLIST      : tactic list -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENLIST"]
-
-(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
-val tclMAP           : ('a -> tactic) -> 'a list -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclMAP"]
-
-(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
-   [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *)
-val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHEN_i"]
-
-(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
-   to the last resulting subgoal (previously called [tclTHENL]) *)
-val tclTHENLAST         : tactic -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENLAST"]
-
-(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
-   to the first resulting subgoal *)
-val tclTHENFIRST         : tactic -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENFIRST"]
-
-(** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
-   [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
-   an error if the number of resulting subgoals is not [n] *)
-val tclTHENSV         : tactic -> tactic array -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENSV"]
-
-(** Same with a list of tactics *)
-val tclTHENS         : tactic -> tactic list -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENS"]
-
-(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
-   applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
-   the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
-   subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
-   error if the number of resulting subgoals is strictly less than [n+m] *)
-val tclTHENS3PARTS     : tactic -> tactic array -> tactic -> tactic array -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENS3PARTS"]
-
-(** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
-   last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
-val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENSLASTn"]
-
-(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
-   applies [t1],...,[tn] on the first [n] resulting subgoals and
-   [tac2] for the remaining last subgoals (previously called tclTHENST) *)
-val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENSFIRSTn"]
-
 (** A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
 (** Takes an exception and either raise it at the next
    level or do nothing. *)
 val catch_failerror  : Exninfo.iexn -> unit
-
-val tclORELSE0       : tactic -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclORELSE0"]
-val tclORELSE        : tactic -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclORELSE"]
-val tclREPEAT        : tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclREPEAT"]
-val tclFIRST         : tactic list -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclFIRST"]
-val tclTRY           : tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTRY"]
-val tclTHENTRY       : tactic -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclTHENTRY"]
-val tclCOMPLETE      : tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclCOMPLETE"]
-val tclAT_LEAST_ONCE : tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclAT_LEAST_ONCE"]
-val tclFAIL          : int -> Pp.t -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclFAIL"]
-val tclFAIL_lazy     : int -> Pp.t Lazy.t -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclFAIL_lazy"]
-val tclDO            : int -> tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclDO"]
-val tclPROGRESS      : tactic -> tactic
-[@@ocaml.deprecated "Use Tactical.New.tclPROGRESS"]
-val tclSHOWHYPS      : tactic -> tactic
-[@@ocaml.deprecated "Internal tactic. Do not use."]
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 22c5bbe73f..d1ee55a677 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -23,39 +23,230 @@ open Tactypes
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-(************************************************************************)
-(* Tacticals re-exported from the Refiner module                        *)
-(************************************************************************)
+(*********************)
+(*   Tacticals       *)
+(*********************)
 
 type tactic = Proofview.V82.tac
 
-[@@@ocaml.warning "-3"]
-
-let tclIDTAC         = Refiner.tclIDTAC
-let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
-let tclORELSE0       = Refiner.tclORELSE0
-let tclORELSE        = Refiner.tclORELSE
-let tclTHEN          = Refiner.tclTHEN
-let tclTHENLIST      = Refiner.tclTHENLIST
-let tclMAP           = Refiner.tclMAP
-let tclTHEN_i        = Refiner.tclTHEN_i
-let tclTHENFIRST     = Refiner.tclTHENFIRST
-let tclTHENLAST      = Refiner.tclTHENLAST
-let tclTHENS         = Refiner.tclTHENS
-let tclTHENSV        = Refiner.tclTHENSV
-let tclTHENSFIRSTn   = Refiner.tclTHENSFIRSTn
-let tclTHENSLASTn    = Refiner.tclTHENSLASTn
-let tclREPEAT        = Refiner.tclREPEAT
-let tclFIRST         = Refiner.tclFIRST
-let tclTRY           = Refiner.tclTRY
-let tclCOMPLETE      = Refiner.tclCOMPLETE
-let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
-let tclFAIL          = Refiner.tclFAIL
-let tclFAIL_lazy     = Refiner.tclFAIL_lazy
-let tclDO            = Refiner.tclDO
-let tclPROGRESS      = Refiner.tclPROGRESS
-let tclSHOWHYPS      = Refiner.tclSHOWHYPS
-let tclTHENTRY       = Refiner.tclTHENTRY
+open Evd
+
+exception FailError = Refiner.FailError
+
+let unpackage glsig = (ref (glsig.sigma)), glsig.it
+
+let repackage r v = {it = v; sigma = !r; }
+
+let apply_sig_tac r tac g =
+  Control.check_for_interrupt (); (* Breakpoint *)
+  let glsigma = tac (repackage r g) in
+  r := glsigma.sigma;
+  glsigma.it
+
+(* [goal_goal_list : goal sigma -> goal list sigma] *)
+let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; }
+
+(* identity tactic without any message *)
+let tclIDTAC gls = goal_goal_list gls
+
+(* the message printing identity tactic *)
+let tclIDTAC_MESSAGE s gls =
+  Feedback.msg_info (hov 0 s); tclIDTAC gls
+
+(* General failure tactic *)
+let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s)
+
+(* The Fail tactic *)
+let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
+
+let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
+
+let start_tac gls =
+  let sigr, g = unpackage gls in
+  (sigr, [g])
+
+let finish_tac (sigr,gl) = repackage sigr gl
+
+(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last
+   m subgoals, and [tac] on the others *)
+let thens3parts_tac tacfi tac tacli (sigr,gs) =
+  let nf = Array.length tacfi in
+  let nl = Array.length tacli in
+  let ng = List.length gs in
+  if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals.");
+  let gll =
+      (List.map_i (fun i ->
+        apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
+        0 gs) in
+    (sigr,List.flatten gll)
+
+(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
+let thensf_tac taci tac = thens3parts_tac taci tac [||]
+
+(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
+let thensi_tac tac (sigr,gs) =
+  let gll =
+    List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
+  (sigr, List.flatten gll)
+
+let then_tac tac = thensf_tac [||] tac
+
+(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+   applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
+   the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
+   subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
+   error if the number of resulting subgoals is strictly less than [n+m] *)
+let tclTHENS3PARTS tac1 tacfi tac tacli gls =
+  finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls)))
+
+(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
+   to [gls] and applies [t1], ..., [tn] to the first [n] resulting
+   subgoals, and [tac2] to the others subgoals. Raises an error if
+   the number of resulting subgoals is strictly less than [n] *)
+let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||]
+
+(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
+   to [gls] and applies [t1], ..., [tn] to the last [n] resulting
+   subgoals, and [tac2] to the other subgoals. Raises an error if the
+   number of resulting subgoals is strictly less than [n] *)
+let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
+
+(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
+   [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
+   number of subgoals is *)
+let tclTHEN_i tac taci gls =
+  finish_tac (thensi_tac taci (then_tac tac (start_tac gls)))
+
+(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [tac2] to every resulting subgoals *)
+let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
+
+(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
+   [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
+   an error if the number of resulting subgoals is not [n] *)
+let tclTHENSV tac1 tac2v =
+  tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||]
+
+let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
+
+(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the last resulting subgoal *)
+let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
+
+(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the first resulting subgoal *)
+let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
+
+(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
+   convenient than [tclTHEN] when [n] is large. *)
+let rec tclTHENLIST = function
+    [] -> tclIDTAC
+  | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
+
+(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+let tclMAP tacfun l =
+  List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
+
+(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
+the goal unchanged *)
+let tclPROGRESS tac ptree =
+  let rslt = tac ptree in
+  if Goal.V82.progress rslt ptree then rslt
+  else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.")
+
+(* Execute tac, show the names of new hypothesis names created by tac
+   in the "as" format and then forget everything. From the logical
+   point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
+   except that it takes the time and memory of tac and prints "as"
+   information). The resulting (unchanged) goals are printed *after*
+   the as-expression, which forces pg to some gymnastic.
+   TODO: Have something similar (better?) in the xml protocol.
+   NOTE: some tactics delete hypothesis and reuse names (induction,
+   destruct), this is not detected by this tactical. *)
+let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
+    : Goal.goal list Evd.sigma =
+  let oldhyps = pf_hyps goal in
+  let rslt:Goal.goal list Evd.sigma = tac goal in
+  let { it = gls; sigma = sigma; } = rslt in
+  let hyps =
+    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
+  let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in
+  let newhyps =
+    List.map
+      (fun hypl -> List.subtract cmp hypl oldhyps)
+      hyps
+  in
+  let s =
+    let frst = ref true in
+    List.fold_left
+    (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
+      ^ (List.fold_left
+           (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc)
+           "" lh))
+    "" newhyps in
+  Feedback.msg_notice
+    (str "<infoH>"
+      ++  (hov 0 (str s))
+      ++  (str "</infoH>"));
+  tclIDTAC goal;;
+
+(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
+let tclORELSE0 t1 t2 g =
+  try
+    t1 g
+  with (* Breakpoint *)
+    | e when CErrors.noncritical e ->
+      let e = Exninfo.capture e in Refiner.catch_failerror e; t2 g
+
+(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
+   then applies t2 *)
+let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
+
+(* applies t1;t2then if t1 succeeds or t2else if t1 fails
+   t2* are called in terminal position (unless t1 produces more than
+   1 subgoal!) *)
+let tclORELSE_THEN t1 t2then t2else gls =
+  match
+    try Some(tclPROGRESS t1 gls)
+    with e when CErrors.noncritical e ->
+      let e = Exninfo.capture e in Refiner.catch_failerror e; None
+  with
+    | None -> t2else gls
+    | Some sgl ->
+        let sigr, gl = unpackage sgl in
+        finish_tac (then_tac t2then  (sigr,gl))
+
+(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
+let tclTRY f = (tclORELSE0 f tclIDTAC)
+
+let tclTHENTRY f g = (tclTHEN f (tclTRY g))
+
+(* Try the first tactic that does not fail in a list of tactics *)
+
+let rec tclFIRST = function
+  | [] -> tclFAIL_s "No applicable tactic."
+  |  t::rest -> tclORELSE0 t (tclFIRST rest)
+
+(* Fails if a tactic did not solve the goal *)
+let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
+
+(* Iteration tacticals *)
+
+let tclDO n t =
+  let rec dorec k =
+    if k < 0 then user_err ~hdr:"Refiner.tclDO"
+      (str"Wrong argument : Do needs a positive integer.");
+    if Int.equal k 0 then tclIDTAC
+    else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1)))
+  in
+  dorec n
+
+
+(* Beware: call by need of CAML, g is needed *)
+let rec tclREPEAT t g =
+  tclORELSE_THEN t (tclREPEAT t) tclIDTAC g
+
+let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
 (************************************************************************)
 (* Tacticals applying on hypotheses                                     *)
@@ -245,10 +436,12 @@ let elimination_sort_of_clause = function
   | None -> elimination_sort_of_goal
   | Some id -> elimination_sort_of_hyp id
 
+(* Change evars *)
+let tclEVARS sigma gls = tclIDTAC {gls with Evd.sigma=sigma}
 
 let pf_with_evars glsev k gls =
   let evd, a = glsev gls in
-    tclTHEN (Refiner.tclEVARS evd) (k a) gls
+    tclTHEN (tclEVARS evd) (k a) gls
 
 let pf_constr_of_global gr k =
   pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k