Try to fail a bit faster in bad reification

1 files changed, 6 insertions, 6 deletions

diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v
index 024eda8d3..df955ddc8 100644
--- a/src/Compilers/Reify.v
+++ b/src/Compilers/Reify.v
@@ -203,12 +203,12 @@ Ltac reifyf base_type_code interp_base_type op var e :=
           let C' := match constr:(Set) with
                     | _ => constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) =>
                                      (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *)
-                    | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to reify by typeclasses:" e)
+                    | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to reify by typeclasses:" e; fail 100)
                     end in
           match constr:(Set) with
           | _ => lazymatch C'
                  with fun _ v _ => @?C v => C end
-          | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to eliminate function dependencies of:" C')
+          | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to eliminate function dependencies of:" C'; fail 100)
           end
         | match ?ev with pair a b => @?eC a b end =>
           let dummy := debug_reifyf_case "matchpair" in
@@ -302,10 +302,10 @@ Ltac reifyf base_type_code interp_base_type op var e :=
                          let args := let a01 := mkPair a0 a1 in let a012 := mkPair a01 a2 in mkPair a012 a3 in
                          mkOp (@Prod _ (@Prod _ (@Prod _ a0T a1T) a2T) a3T) tR op_code args
                     end
-               | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: Unsupported number of operation arguments in reifyf:" nargs)
+               | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: Unsupported number of operation arguments in reifyf:" nargs; fail 100)
                end
           | reification_unsuccessful
-            => constr_run_tac_fail ltac:(fun _ => idtac "Error: Failed to reify:" x)
+            => constr_run_tac_fail ltac:(fun _ => idtac "Error: Failed to reify:" x; fail 100)
           end
         end in
     let dummy := debug_leave_reifyf_success e ret in
@@ -348,12 +348,12 @@ Ltac reify_abs base_type_code interp_base_type op var e :=
       let C' := match constr:(Set) with
                 | _ => constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) =>
                                  (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *)
-                | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_absB: Failed to reify by typeclasses:" e)
+                | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_abs: Failed to reify by typeclasses:" e; fail 100)
                 end in
       let C := match constr:(Set) with
                | _ => lazymatch C'
                       with fun _ v _ => @?C v => C end
-               | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_abs: Failed to eliminate function dependencies of:" C')
+               | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_abs: Failed to eliminate function dependencies of:" C'; fail 100)
                end in
       mkAbs t C
     | ?x =>