Module Ltac2_plugin.Tac2typing_env

module TVar : sig ... end
type t
val empty_env : ?⁠strict:bool -> unit -> t

default strict:true

val set_rec : (Names.KerName.t * int) Names.Id.Map.t -> t -> t
val reject_unbound_tvar : t -> t
val env_strict : t -> bool
val env_name : t -> TVar.t -> string
val fresh_id : t -> TVar.t
val get_alias : Names.lident -> t -> TVar.t
val find_rec_var : Names.Id.t -> t -> (Names.KerName.t * int) option
type mix_var =
| GVar of TVar.t
| LVar of int
type mix_type_scheme = int * mix_var Tac2expr.glb_typexpr
val mem_var : Names.Id.t -> t -> bool
val find_var : Names.Id.t -> t -> mix_type_scheme
val bound_vars : t -> Names.Id.Set.t
val get_variable0 : (Names.Id.t -> bool) -> Tac2expr.tacref Tac2expr.or_relid -> Tac2expr.tacref Locus.or_var
val get_variable : t -> Tac2expr.tacref Tac2expr.or_relid -> Tac2expr.tacref Locus.or_var
val kind : t -> TVar.t Tac2expr.glb_typexpr -> TVar.t Tac2expr.glb_typexpr

View function, allows to ensure head normal forms

val pr_glbtype : t -> TVar.t Tac2expr.glb_typexpr -> Pp.t
val eq_or_tuple : ('a -> 'b -> bool) -> 'a Tac2expr.or_tuple -> 'b Tac2expr.or_tuple -> bool
exception CannotUnify of TVar.t Tac2expr.glb_typexpr * TVar.t Tac2expr.glb_typexpr
val unify0 : t -> TVar.t Tac2expr.glb_typexpr -> TVar.t Tac2expr.glb_typexpr -> unit

unify0 raises CannotUnify, unify raises usererror

val unify : ?⁠loc:Loc.t -> t -> TVar.t Tac2expr.glb_typexpr -> TVar.t Tac2expr.glb_typexpr -> unit
val unify_arrow : ?⁠loc:Loc.t -> t -> TVar.t Tac2expr.glb_typexpr -> (Loc.t option * TVar.t Tac2expr.glb_typexpr) list -> TVar.t Tac2expr.glb_typexpr
val abstract_var : t -> TVar.t Tac2expr.glb_typexpr -> mix_type_scheme
val monomorphic : TVar.t Tac2expr.glb_typexpr -> mix_type_scheme
val polymorphic : Tac2expr.type_scheme -> mix_type_scheme
val push_name : Names.Name.t -> mix_type_scheme -> t -> t
val push_ids : mix_type_scheme Names.Id.Map.t -> t -> t
val subst_type : ('a -> 'b Tac2expr.glb_typexpr) -> 'a Tac2expr.glb_typexpr -> 'b Tac2expr.glb_typexpr
val normalize : t -> (int Stdlib.ref * int Tac2expr.glb_typexpr TVar.Map.t Stdlib.ref) -> TVar.t Tac2expr.glb_typexpr -> int Tac2expr.glb_typexpr