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

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

unify0 raises CannotUnify, unify raises usererror

val unify : ?loc:Loc.t -> t -> TVar.t Tac2expr.glb_typexpr -> TVar.t Tac2expr.glb_typexpr -> unit
val abstract_var : t -> TVar.t Tac2expr.glb_typexpr -> 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