package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587

doc/coq-core.engine/Proofview_monad/P/index.html

Module Proofview_monad.PSource

Sourcetype w = bool

Status (safe/unsafe) * given up

Sourceval wunit : w
Sourceval wprod : w -> w -> w
Sourcetype e = {
  1. trace : bool;
  2. name : Names.Id.t;
  3. poly : bool;
}

Recording info trace (true) or not.

Sourceval uunit : u
OCaml

Innovation. Community. Security.