Tac2typing_env (coq-core.Ltac2_plugin.Tac2typing

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