Typing (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.rocq-runtime.pretyping.Typing)

Source

val type_of : 
  ?refresh:bool ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Evd.evar_map * EConstr.types

Typecheck a term and return its type + updated evars, optionally refreshing universes

Source

val sort_of : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Evd.evar_map * EConstr.ESorts.t

Typecheck a type and return its sort

Source

val check : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.types ->
  Evd.evar_map

Typecheck a term has a given type (assuming the type is OK)

Sourceval type_of_variable : Environ.env -> Names.variable -> EConstr.types

Type of a variable.

Source

val solve_evars : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Solve existential variables using typing

Source

val check_allowed_sort : 
  Environ.env ->
  Evd.evar_map ->
  Names.inductive EConstr.puniverses ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.ERelevance.t

Raise an error message if incorrect elimination for this inductive (first constr is term to match, second is return predicate)

Source

val check_type_fixpoint : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t EConstr.binder_annot array ->
  EConstr.types array ->
  EConstr.unsafe_judgment array ->
  Evd.evar_map

Raise an error message if bodies have types not unifiable with the expected ones

Source

val check_actual_type : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.unsafe_judgment ->
  EConstr.types ->
  Evd.evar_map

Variant of check that assumes that the argument term is well-typed.

Source

val type_judgment : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.unsafe_judgment ->
  Evd.evar_map * EConstr.unsafe_type_judgment

Sourceval judge_of_sprop : EConstr.unsafe_judgment

Sourceval judge_of_prop : EConstr.unsafe_judgment

Sourceval judge_of_set : EConstr.unsafe_judgment

Sourceval judge_of_variable : Environ.env -> Names.Id.t -> EConstr.unsafe_judgment

Source

val judge_of_apply : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.unsafe_judgment ->
  EConstr.unsafe_judgment array ->
  Evd.evar_map * EConstr.unsafe_judgment

Source

val judge_of_abstraction : 
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t ->
  EConstr.unsafe_type_judgment ->
  EConstr.unsafe_judgment ->
  EConstr.unsafe_judgment

Source

val judge_of_product : 
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t ->
  EConstr.unsafe_type_judgment ->
  EConstr.unsafe_type_judgment ->
  EConstr.unsafe_judgment

Source

val judge_of_projection : 
  Environ.env ->
  Evd.evar_map ->
  Names.Projection.t ->
  EConstr.unsafe_judgment ->
  EConstr.unsafe_judgment

Sourceval judge_of_int : Environ.env -> Uint63.t -> EConstr.unsafe_judgment

Sourceval judge_of_float : Environ.env -> Float64.t -> EConstr.unsafe_judgment

Sourceval judge_of_string : Environ.env -> Pstring.t -> EConstr.unsafe_judgment

Source

val checked_appvect : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr array ->
  Evd.evar_map * EConstr.constr

Source

val checked_applist : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr list ->
  Evd.evar_map * EConstr.constr

Source

val recheck_against : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map * EConstr.types

hack

Sourcetype ('constr, 'types, 'r) bad_relevance =

| BadRelevanceBinder of 'r * ('constr, 'types, 'r) Context.Rel.Declaration.pt
| BadRelevanceCase of 'r * 'constr

Source

val bad_relevance_msg : 
  (Environ.env
   * Evd.evar_map
   * (EConstr.constr, EConstr.types, EConstr.ERelevance.t) bad_relevance)
    CWarnings.msg

Source

val get_template_parameters : 
  Environ.env ->
  Evd.evar_map ->
  Names.inductive ->
  EConstr.unsafe_judgment array ->
  Evd.evar_map * Inductive.param_univs