diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-30 14:50:59 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-01 22:43:57 +0100 |
| commit | bfa71dfcf722dfc0e1f1cd616945cc3e1da9d5ba (patch) | |
| tree | 9f0e2d59404a8cf63f44b7dc7d31eb2a10286003 /proofs/pfedit.ml | |
| parent | d47c178be6e5dc52fedbb312fc51673623608994 (diff) | |
Info: do not record info trace unless needed.
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c5eb03d5f..09d94a9ce 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -92,6 +92,10 @@ let solve ?with_end_tac gi info_lvl tac pr = let tac = match with_end_tac with | None -> tac | Some etac -> Proofview.tclTHEN tac etac in + let tac = match info_lvl with + | None -> tac + | Some _ -> Proofview.Trace.record_info_trace tac + in let tac = match gi with | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac |