Skip to content

Commit

Permalink
Control.once in debug_profile (#76)
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross authored Oct 6, 2022
1 parent 7daccb3 commit 890df0f
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Rewriter/Language/Reify.v
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,8 @@ Module Compilers.
:= debug_if should_debug_typing_failure_assume_well_typed (fun () => printf "Warning: %s: could not well-type %t due to underlying issue typechecking %t without relevant context %a, but assuming that it's well-typed because %t is not a template-parameter type" funname v term (fun () => Message.of_list Message.of_binder) ctx_tys ty) ().
Ltac2 debug_profile (descr : string) (f : unit -> 'a) : 'a
:= if should_debug_profile ()
then Control.time (Some descr) f
else f ().
then Control.once (fun () => Control.time (Some descr) f)
else Control.once f.
Ltac2 debug_fine_grained (funname : string) (msg : unit -> message)
:= debug_if should_debug_fine_grained (fun () => printf "%s: %a" funname (fun () => msg) ()) ().
Ltac2 debug_enter_reify (funname : string) (e : constr)
Expand Down

0 comments on commit 890df0f

Please sign in to comment.