Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_4495.v Sprache: Coq

Original von: Coq^©

Require Import Coq.ZArith.ZArith.
Ltac profile_constr tac :=
  let dummy := match goal with _ => reset ltac profile; start ltac profiling end in
  let ret := match goal with _ => tac () end in
  let dummy := match goal with _ => stop ltac profiling; show ltac profile end in
  pose 1.

Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl).

Goal True.
  start ltac profiling.
  reset ltac profile.
  reset ltac profile.
  stop ltac profiling.
  time profile_constr slow.
  show ltac profile cutoff 0.
  show ltac profile "slow".
Abort.

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.