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_side_condition
type implicits_list = implicit_side_condition * implicit_status list
val is_status_implicit : implicit_status -> bool
val binding_kind_of_status : implicit_status -> Glob_term.binding_kind
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_implicits = (Names.Name.t * bool) option CAst.t 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 -> impl:Glob_term.binding_kind -> 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 -> unit
val maybe_declare_manual_implicits : bool -> Names.GlobRef.t -> ?enriching:bool -> manual_implicits -> unit
val set_implicits : bool -> Names.GlobRef.t -> (Names.Name.t * Glob_term.binding_kind) list list -> 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 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