diff options
Diffstat (limited to 'src/Util/SideConditions/CorePackages.v')
-rw-r--r-- | src/Util/SideConditions/CorePackages.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v new file mode 100644 index 000000000..19612df0a --- /dev/null +++ b/src/Util/SideConditions/CorePackages.v @@ -0,0 +1,16 @@ +Import EqNotations. + +Record evar_package {T} (v : T) := + { val : T; + evar_package_pf : val = v }. +Arguments val {T v} _. +Arguments evar_package_pf {T v} _. +Record evard_package {s d} (v : s) := + { vald : d; + evard_package_pfT : s = d; + evard_package_pf : vald = rew evard_package_pfT in v }. +Arguments vald {s d v} _. +Arguments evard_package_pfT {s d v} _. +Arguments evard_package_pf {s d v} _. + +Ltac autosolve else_tac := else_tac (). |