package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/coq-core.vernac/Locality/index.html

Module LocalitySource

* Managing locality

Sourcetype import_status =
  1. | ImportDefaultBehavior
  2. | ImportNeedQualified
Sourcetype locality =
  1. | Discharge
  2. | Global of import_status

* Positioning locality for commands supporting discharging and export outside of modules

For commands whose default is to discharge and export: Global is the default and is neutral; Local in a section deactivates discharge, Local not in a section deactivates export

Sourceval make_locality : bool option -> bool
Sourceval make_non_locality : bool option -> bool
Sourceval enforce_locality_exp : bool option -> Vernacexpr.discharge -> locality
Sourceval enforce_locality : bool option -> bool

For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; Local in sections is the default, Local not in section forces non-export

Sourceval make_section_locality : bool option -> bool
Sourceval enforce_section_locality : bool option -> bool

* Positioning locality for commands supporting export but not discharge

For commands whose default is to export (if not in section): Global in sections is forbidden, Global not in section is neutral; Local in sections is the default, Local not in section forces non-export

Sourceval make_module_locality : bool option -> bool
Sourceval enforce_module_locality : bool option -> bool
OCaml

Innovation. Community. Security.