package coq

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

Module PrimredSource

Sourcetype _ action_kind =
  1. | IncompatTypes : _ CPrimitives.prim_type -> Names.Constant.t action_kind
  2. | IncompatInd : _ CPrimitives.prim_ind -> Names.inductive action_kind

Reduction of primitives

Sourcetype exn +=
  1. | IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
Sourceval add_retroknowledge : Environ.env -> Retroknowledge.action -> Environ.env

May raise IncomtibleDeclarations

Sourceval get_int_type : Environ.env -> Names.Constant.t
Sourceval get_float_type : Environ.env -> Names.Constant.t
Sourceval get_cmp_type : Environ.env -> Names.Constant.t
Sourceval get_bool_constructors : Environ.env -> Names.constructor * Names.constructor
Sourceval get_carry_constructors : Environ.env -> Names.constructor * Names.constructor
Sourceval get_pair_constructor : Environ.env -> Names.constructor
Sourceexception NativeDestKO
Sourcemodule type RedNativeEntries = sig ... end
Sourcemodule type RedNative = sig ... end
Sourcemodule RedNative (E : RedNativeEntries) : RedNative with type elem = E.elem with type args = E.args with type evd = E.evd with type uinstance = E.uinstance
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