package rocq-runtime

  1. Overview
  2. Docs

Module Ltac2_plugin.Tac2typing_envSource

Sourcemodule TVar : sig ... end
Sourcetype t
Sourceval empty_env : ?strict:bool -> ?accumulate_errors:bool -> UnivNames.universe_binders -> unit -> t

default strict:true, accumulate_errors:false

Sourceval add_error : ?loc:Loc.t -> t -> Pp.t -> unit

In accumulate mode, add the error to the list in the env. Otherwise raise UserError.

Sourceval get_errors : t -> Pp.t Loc.located list

Get accumulated errors. Assertion failure if not in accumulate mode.

Sourceval scopes : t -> Tac2syn.Tac2Scope.t list
Sourceval set_rec : (Names.KerName.t * int) Names.Id.Map.t -> t -> t
Sourceval reject_unbound_tvar : t -> t
Sourceval env_strict : t -> bool
Sourceval env_name : t -> TVar.t -> string
Sourceval fresh_id : t -> TVar.t
Sourceval get_alias : Names.lident -> t -> TVar.t
Sourceval find_rec_var : Names.Id.t -> t -> (Names.KerName.t * int) option
Sourcetype mix_var =
  1. | GVar of TVar.t
  2. | LVar of int
Sourcetype mix_type_scheme = int * mix_var Tac2expr.glb_typexpr
Sourceval mem_var : Names.Id.t -> t -> bool
Sourceval find_var : Names.Id.t -> t -> mix_type_scheme
Sourceval is_used_var : Names.Id.t -> t -> bool
Sourceval bound_vars : t -> Names.Id.Set.t

View function, allows to ensure head normal forms

Sourceval pr_glbtype : t -> TVar.t Tac2expr.glb_typexpr -> Pp.t
Sourceval eq_or_tuple : ('a -> 'b -> bool) -> 'a Tac2expr.or_tuple -> 'b Tac2expr.or_tuple -> bool

unify0 raises CannotUnify, unify raises usererror

Sourceval push_name : Names.Name.t -> mix_type_scheme -> t -> t
Sourceval normalize : t -> (int Stdlib.ref * int Tac2expr.glb_typexpr TVar.Map.t Stdlib.ref) -> TVar.t Tac2expr.glb_typexpr -> int Tac2expr.glb_typexpr