package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val make_implicit_args : bool -> unit
val make_strict_implicit_args : bool -> unit
val make_strongly_strict_implicit_args : bool -> unit
val make_reversible_pattern_implicit_args : bool -> unit
val make_contextual_implicit_args : bool -> unit
val make_maximal_implicit_args : bool -> unit
val is_implicit_args : unit -> bool
val is_strict_implicit_args : unit -> bool
val is_strongly_strict_implicit_args : unit -> bool
val is_reversible_pattern_implicit_args : unit -> bool
val is_contextual_implicit_args : unit -> bool
val is_maximal_implicit_args : unit -> bool
val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
type argument_position =
  1. | Conclusion
  2. | Hyp of int
type implicit_explanation =
  1. | DepRigid of argument_position
  2. | DepFlex of argument_position
  3. | DepFlexAndRigid of argument_position * argument_position
  4. | Manual
type maximal_insertion = bool
type force_inference = bool
type implicit_status = (Names.Id.t * implicit_explanation * (maximal_insertion * force_inference)) option
type implicit_side_condition
type implicits_list = implicit_side_condition * implicit_status list
val is_status_implicit : implicit_status -> bool
val is_inferable_implicit : bool -> int -> implicit_status -> bool
val name_of_implicit : implicit_status -> Names.Id.t
val maximal_insertion_of : implicit_status -> bool
val force_inference_of : implicit_status -> bool
val positions_of_implicits : implicits_list -> int list
type manual_explicitation = Constrexpr.explicitation * (maximal_insertion * force_inference * bool)
type manual_implicits = manual_explicitation list
val compute_implicits_with_manual : Environ.env -> Evd.evar_map -> EConstr.types -> bool -> manual_implicits -> implicit_status list
val compute_implicits_names : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t list
val declare_var_implicits : Names.variable -> unit
val declare_constant_implicits : Names.Constant.t -> unit
val declare_mib_implicits : Names.MutInd.t -> unit
val declare_implicits : bool -> Names.GlobRef.t -> unit
val declare_manual_implicits : bool -> Names.GlobRef.t -> ?enriching:bool -> manual_implicits list -> unit
val maybe_declare_manual_implicits : bool -> Names.GlobRef.t -> ?enriching:bool -> manual_implicits -> unit
val implicits_of_global : Names.GlobRef.t -> implicits_list list
val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list
val lift_implicits : int -> manual_implicits -> manual_implicits
val make_implicits_list : implicit_status list -> implicits_list list
val drop_first_implicits : int -> implicits_list -> implicits_list
val projection_implicits : Environ.env -> Names.Projection.t -> implicit_status list -> implicit_status list
val select_impargs_size : int -> implicits_list list -> implicit_status list
val select_stronger_impargs : implicits_list list -> implicit_status list
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
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