package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Proof_usingSource

Utility code for section variables handling in Proof using...

At some point it would be good to make this abstract

Sourceval definition_using : Environ.env -> Evd.evar_map -> using:Vernacexpr.section_subset_expr -> terms:EConstr.constr list -> t

Process a using expression in definitions to provide the list of used terms

Sourceval suggest_constant : Environ.env -> Names.Constant.t -> unit
Sourceval suggest_variable : Environ.env -> Names.Id.t -> unit
Sourceval get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
Sourceval proof_using_opt_name : string list

For the stm

Sourceval using_from_string : string -> Vernacexpr.section_subset_expr
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct