diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-17 11:32:48 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-17 11:32:48 -0400 |
commit | 17b018fe9d134028da41f397c41d1f4149dfe742 (patch) | |
tree | 17f58dbf449cfbf39479d40e1af628fa36f68148 /src/Compilers/Reify.v | |
parent | 41b0cf02cc291eaf2597b4f68339450ac363f969 (diff) |
Remove fails; if we fail too strongly, we miss debugging information
Diffstat (limited to 'src/Compilers/Reify.v')
-rw-r--r-- | src/Compilers/Reify.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v index df955ddc8..b986722f8 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; fail 100) + | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to reify by typeclasses:" e) 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'; fail 100) + | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reifyf: Failed to eliminate function dependencies of:" C') 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; fail 100) + | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: Unsupported number of operation arguments in reifyf:" nargs) end | reification_unsuccessful - => constr_run_tac_fail ltac:(fun _ => idtac "Error: Failed to reify:" x; fail 100) + => constr_run_tac_fail ltac:(fun _ => idtac "Error: Failed to reify:" x) 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_abs: Failed to reify by typeclasses:" e; fail 100) + | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_abs: Failed to reify by typeclasses:" e) 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'; fail 100) + | _ => constr_run_tac_fail ltac:(fun _ => idtac "Error: reify_abs: Failed to eliminate function dependencies of:" C') end in mkAbs t C | ?x => |