package coq-core

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

Module UnivGenSource

Sourcetype univ_length_mismatch = {
  1. actual : int * int;
  2. expect : int * int;
}
Sourceexception UniverseLengthMismatch of univ_length_mismatch

Side-effecting functions creating new universe levels.

Sourceval new_univ_global : unit -> Univ.UGlobal.t
Sourceval new_sort_global : unit -> Sorts.QVar.t
Sourceval fresh_level : unit -> Univ.Level.t

Build a fresh instance for a given context, its associated substitution and the instantiated constraints.

Sourcetype 'a in_sort_context_set = 'a * sort_context_set
Sourceval empty_sort_context : sort_context_set
Sourceval is_empty_sort_context : sort_context_set -> bool
Sourceval fresh_sort_in_family : Sorts.family -> Sorts.t in_sort_context_set

NB: InQSort is treated as InType

Sourceval fresh_global_instance : ?loc:Loc.t -> ?names:UVars.Instance.t -> Environ.env -> Names.GlobRef.t -> Constr.constr in_sort_context_set
Sourceval fresh_universe_context_set_instance : Univ.ContextSet.t -> Univ.universe_level_subst * Univ.ContextSet.t

Get fresh variables for the universe context. Useful to make tactics that manipulate constrs in universe contexts polymorphic.

Sourceval fresh_sort_context_instance : sort_context_set -> UVars.sort_level_subst * sort_context_set
Sourceval constr_of_monomorphic_global : Environ.env -> Names.GlobRef.t -> Constr.constr

Create a fresh global in the environment argument, without side effects. BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for the proper way to get a fresh copy of a polymorphic global reference.

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