diff options
| author | Arnaud Spiwack | 2014-10-30 14:50:59 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | bfa71dfcf722dfc0e1f1cd616945cc3e1da9d5ba (patch) | |
| tree | 9f0e2d59404a8cf63f44b7dc7d31eb2a10286003 /proofs/proofview_monad.mli | |
| parent | d47c178be6e5dc52fedbb312fc51673623608994 (diff) | |
Info: do not record info trace unless needed.
Diffstat (limited to 'proofs/proofview_monad.mli')
| -rw-r--r-- | proofs/proofview_monad.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli index ef20415ceb..8a2f950142 100644 --- a/proofs/proofview_monad.mli +++ b/proofs/proofview_monad.mli @@ -81,7 +81,8 @@ module P : sig val wunit : w val wprod : w -> w -> w - type e = unit + (** Recording info trace (true) or not. *) + type e = bool type u = Info.state @@ -130,6 +131,9 @@ module Giveup : Writer with type t = Evar.t list (** Lens and utilies pertaining to the info trace *) module InfoL : sig + (** [record_trace t] behaves like [t] and compute its [info] trace. *) + val record_trace : 'a Logical.t -> 'a Logical.t + val update : (Info.state -> Info.state) -> unit Logical.t val opn : Info.tag -> unit Logical.t val close : unit Logical.t |