package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

doc/coq-core.stm/ProofBlockDelimiter/index.html

Module ProofBlockDelimiterSource

Sourceval simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool

A goal is simple if it nor depends on nor impacts on any other goal. This function is used to detect, dynamically, if a proof block leaks, i.e. if skipping it could impact other goals (like not instantiating their type). `Simple carries the list of focused goals.

Sourceval is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
Sourcetype 'a until = [
  1. | `Stop
  2. | `Found of Stm.static_block_declaration
  3. | `Cont of 'a
]
Sourceval crawl : Stm.document_view -> ?init:Stm.document_node option -> ('a -> Stm.document_node -> 'a until) -> 'a -> Stm.static_block_declaration option