open Preamble

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open List

open Lists

open Bool

open Relations

open Nat

open Positive

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Identifiers

open Order

type register = PreIdentifiers.identifier

(** val register_eq : register -> register -> (__, __) Types.sum **)
let register_eq =
  Identifiers.identifier_eq PreIdentifiers.RegisterTag

type 'a register_env = 'a Identifiers.identifier_map