package coq-core

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

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

At some point it would be good to make this abstract

val 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

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

For the stm

val 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