Constructor tactics backtracking is done using [Tacticals.New] rather than [Proofview].

The primitives in [Tacticals] respect Ltac's error level, whereas the one in [Proofview] do not necessarily. In that case the error caught was ignored causing arbitrary error level after [constructor] to be canceled.

Needed the addition of an [ORD] variant to [OR] in [Tacticals.New] to avoid unnecessary precomputation (the 'D' stands for 'delay').

Fixes #3838.

3 files changed, 15 insertions, 1 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 97e2373b7e..9256e10d60 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -326,6 +326,15 @@ module New = struct
         end
     end
 
+  let tclORD t1 t2 =
+    tclINDEPENDENT begin
+      Proofview.tclOR
+        t1
+        begin fun e ->
+          catch_failerror e <*> t2 ()
+        end
+    end
+
   let tclONCE = Proofview.tclONCE
 
   let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index d6630bb79b..35a3205896 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -169,6 +169,11 @@ module New : sig
   (** Fail with a [User_Error] containing the given message. *)
 
   val tclOR : unit tactic -> unit tactic -> unit tactic
+  val tclORD : unit tactic -> (unit -> unit tactic) -> unit tactic
+  (** Like {!tclOR} but accepts a delayed tactic as a second argument
+      in the form of a function which will be run only in case of
+      backtracking. *)
+
   val tclONCE : unit tactic -> unit tactic
   val tclEXACTLY_ONCE : unit tactic -> unit tactic
   val tclORELSE0 : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c28295b0fa..f1b5424818 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1911,7 +1911,7 @@ let one_constructor i lbind = constructor_tac false None i lbind
 let rec tclANY tac = function
 | [] -> Tacticals.New.tclZEROMSG (str "No applicable tactic.")
 | arg :: l ->
-  Proofview.tclOR (tac arg) (fun _ -> tclANY tac l)
+  Tacticals.New.tclORD (tac arg) (fun () -> tclANY tac l)
 
 let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in