`Unification`#

Ltac2.Unification

type conv_flag = private ..

Controls if cumulativity Prop ≤ Set ≤ Type 1 ≤ … ≤ Type i ≤ … is used for conversion.

See Conversion.conv_pb.

type conv_flag +=

| Cumulative
(*
Enables cumulativity Prop ≤ Set ≤ Type 1 ≤ … ≤ Type i ≤ … for conversion.
*)
| Conv
(*
Does not enable cumulativity Prop ≤ Set ≤ Type 1 ≤ … ≤ Type i ≤ … for conversion.
*)

val conv :
  Environ.env ->
  Evd.evar_map ->
  conv_flag ->
  TransparentState.t ->
  constr ->
  constr ->
  Evd.evar_map option

conv env sigma flag ts c1 c2 returns Some sigma if both c1 and c2 are convertible, in which case sigma is the updated evar map with the universe constraints required for the terms to be convertible. It returns None if the terms are not convertible.

conv is parametrized by:

flag which controls if conversion is done up to cumulativity or not.
ts which controls which constants get unfolded during conversion.

val unify : TransparentState.t -> constr -> constr -> unit Proofview.tactic

unify ts c1 c2 unifies c1 and c2 (using Evarconv unification), which may have the effect of instantiating evars. If c1 and c2 cannot be unified, the tactic fails.

val solve_constraints : unit Proofview.tactic

solve_constraints solves any delayed unification constraints.

Unification#

`Unification`#