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