Flags

Ltac2.Constr.Pretype.Flags

type t = Pretyping.inference_flags

Flags used to control pretyping.

val constr_flags : t

Flags used by constr:(…).

val set_use_coercions : bool -> t -> t

Sets use of coercions during pretyping.

true in constr_flags.

val set_use_typeclasses : bool -> t -> t

Sets whether to run typeclass inference at the end of pretyping and when needed according to the "Typeclass Resolution For Conversion" flag.

true in constr_flags.

val set_allow_evars : bool -> t -> t

Sets whether to allow pretyping to produce new unresolved evars.

false in constr_flags.

val set_nf_evars : bool -> t -> t

Sets whether to evar-normalize the result of pretyping. This should not impact anything other than performance.

true in constr_flags.