blob: 14b02b766b41d133802dde5877b7e3bb44ec723a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Crypto.Util.TagList.
Module Type PrePackage.
Parameter package : Tag.Context.
End PrePackage.
Module MakePackageBase (PKG : PrePackage).
Ltac get_package _ := eval hnf in PKG.package.
Ltac get key :=
let pkg := get_package () in
Tag.get pkg key.
End MakePackageBase.
|
