Code simplification in Tactics.

1 files changed, 51 insertions, 44 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6dc219ae6c..3038a95068 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1358,7 +1358,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       | None -> None
   in elim
 
-let descend_in_conjunctions avoid tac exit c =
+let descend_in_conjunctions avoid tac (err, info) c =
   Proofview.Goal.nf_enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -1392,8 +1392,8 @@ let descend_in_conjunctions avoid tac exit c =
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
            end))
-    | None -> exit ()
-  with RefinerError _|UserError _ -> exit ()
+    | None -> Proofview.tclZERO ~info err
+  with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
   end
 
 (****************************************************)
@@ -1416,7 +1416,15 @@ let solve_remaining_apply_goals =
     with Not_found -> Proofview.tclUNIT ()
   else Proofview.tclUNIT ()
   end
-  
+
+let tclORELSEOPT t k =
+  Proofview.tclORELSE t
+    (fun e -> match k e with
+    | None ->
+      let (e, info) = e in
+      Proofview.tclZERO ~info e
+    | Some tac -> tac)
+
 let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
   Proofview.Goal.nf_enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
@@ -1441,47 +1449,46 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
       with UserError _ as exn ->
         Proofview.tclZERO exn
     in
-    Proofview.tclORELSE
+    let rec try_red_apply thm_ty (exn0, info) =
+      try
+        (* Try to head-reduce the conclusion of the theorem *)
+        let red_thm = try_red_product env sigma thm_ty in
+        tclORELSEOPT
+          (try_apply red_thm concl_nprod)
+          (function (e, info) -> match e with
+          | PretypeError _|RefinerError _|UserError _|Failure _ ->
+            Some (try_red_apply red_thm (exn0, info))
+          | _ -> None)
+      with Redelimination ->
+        (* Last chance: if the head is a variable, apply may try
+            second order unification *)
+        let info = Loc.add_loc info loc in
+        let tac =
+          if with_destruct then
+            descend_in_conjunctions []
+              (fun b id ->
+                Tacticals.New.tclTHEN
+                  (try_main_apply b (mkVar id))
+                  (Proofview.V82.tactic (thin [id])))
+              (exn0, info) c
+          else
+            Proofview.tclZERO ~info exn0 in
+        if not (Int.equal concl_nprod 0) then
+          tclORELSEOPT
+            (try_apply thm_ty 0)
+            (function (e, info) -> match e with
+            | PretypeError _|RefinerError _|UserError _|Failure _->
+              Some tac
+            | _ -> None)
+        else
+          tac
+    in
+    tclORELSEOPT
       (try_apply thm_ty0 concl_nprod)
       (function (e, info) -> match e with
-        | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
-	let rec try_red_apply thm_ty =
-          try 
-            (* Try to head-reduce the conclusion of the theorem *)
-            let red_thm = try_red_product env sigma thm_ty in
-            Proofview.tclORELSE
-              (try_apply red_thm concl_nprod)
-              (function (e, info) -> match e with
-              | PretypeError _|RefinerError _|UserError _|Failure _ ->
-		try_red_apply red_thm
-              | exn -> iraise (exn, info))
-          with Redelimination ->
-            (* Last chance: if the head is a variable, apply may try
-	       second order unification *)
-            let tac =
-	      if with_destruct then
-                descend_in_conjunctions []
-                  (fun b id ->
-                    Tacticals.New.tclTHEN
-                      (try_main_apply b (mkVar id))
-                      (Proofview.V82.tactic (thin [id])))
-                  (fun _ ->
-                    let info = Loc.add_loc info loc in
-                    Proofview.tclZERO ~info exn0) c
-	      else
-                let info = Loc.add_loc info loc in
-		Proofview.tclZERO ~info exn0 in
-            if not (Int.equal concl_nprod 0) then
-                Proofview.tclORELSE
-                  (try_apply thm_ty 0)
-                  (function (e, info) -> match e with
-                  | PretypeError _|RefinerError _|UserError _|Failure _->
-                    tac
-                  | exn -> iraise (exn, info))
-            else
-              tac
-	in try_red_apply thm_ty0
-      | exn -> iraise (exn, info))
+      | PretypeError _|RefinerError _|UserError _|Failure _ ->
+        Some (try_red_apply thm_ty0 (e, info))
+      | _ -> None)
     end
   in
     Tacticals.New.tclTHENLIST [
@@ -1595,7 +1602,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
       let (e, info) = Errors.push e in
         (descend_in_conjunctions [targetid]
            (fun b id -> aux (id::idstoclear) b (mkVar id))
-           (fun _ -> Proofview.tclZERO ~info e) c)
+           (e, info) c)
     end
   in
   aux [] with_destruct d