Refiner (cooltt.Core.Refiner)

module D := CodeUnit.Domain

module S := CodeUnit.Syntax

module RM := Monads.RefineM

type ('a, 'b) quantifier = 'a -> (Ident.t * (Tactic.var -> 'b)) -> 'b

module Hole : sig ... end

module Probe : sig ... end

module Dim : sig ... end

module Cof : sig ... end

module Prf : sig ... end

module Univ : sig ... end

module El : sig ... end

module ElV : sig ... end

module ElHCom : sig ... end

module Pi : sig ... end

module Sg : sig ... end

module Telescope : sig ... end

module KanTelescope : sig ... end

module Signature : sig ... end

module Sub : sig ... end

module Nat : sig ... end

module Circle : sig ... end

module Structural : sig ... end