(***************************************************************************
* Bundles of Modules for Developments in Programming Language Metatheory   *
* Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1                  *
***************************************************************************)

Require Export 
  LibTactics
  Metatheory_Var 
  Metatheory_Fresh 
  Metatheory_Tactics.

Require Export Metatheory_Env.

Open Scope fset_scope.
Open Scope env_scope.


(* Note: for developement purposes, you may tell Coq to simply 
         assume any subgoal related to freshness, as follows:
     Hint Extern 1 (_ \notin _) => skip.
     Hint Extern 1 (fresh _ _ _) => skip.
*)