`Pretype`#

Ltac2.Constr.Pretype

type expected_type = Pretyping.typing_constraint

Typing constraints for pretyping.

module Flags : sig ... end

val expected_istype : expected_type

Pretyping constraint for terms expected to be types.

val expected_oftype : constr -> expected_type

Pretyping constraint for terms expected to have a specific type.

val expected_without_type_constraint : expected_type

No pretyping constraint.

val pretype :
  Environ.env ->
  Evd.evar_map ->
  Flags.t ->
  expected_type ->
  preterm ->
  Evd.evar_map * constr

pretype env sigma flags type_constraint preterm pretypes the given preterm using the pretyping flags and expected type constraint.

Pretype#