Library CompOptCert.Loc

Require Import Orders.
Require Import Lia.
Require Import Coq.Logic.PropExtensionality.

Require Import sflib.

Require Import DataStructure.
Require Import Basic.

Set Implicit Arguments.

Module Loc := Ident.
Module LocSet := IdentSet.
Module LocMap := IdentMap.
Module LocFun := IdentFun.