diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-07 20:25:30 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-07 20:25:30 -0500 |
commit | f4b9bf1646e0b37541ebde5b030a90f4c762173b (patch) | |
tree | f8669f97391c6a23a6342066ce399a36a6b2c411 /src | |
parent | e9fe0e2cbb98f6b8dcd7c15c7a850bb76f91e8a7 (diff) |
Base evard_package on evar_rel_package
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/SideConditions/CorePackages.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v index ad0756f89..7af4cc133 100644 --- a/src/Util/SideConditions/CorePackages.v +++ b/src/Util/SideConditions/CorePackages.v @@ -25,9 +25,11 @@ Definition evar_package_pf_rel {A v B R} (pkg : @evar_rel_package A v B R) := Eval hnf in evar_package_pf pkg. Definition evard_package {s d} (v : s) - := @evar_Prop_package + := @evar_rel_package + s + v d - (fun vald => { pf : s = d | vald = rew pf in v }). + (fun vald v => { pf : s = d | vald = rew pf in v }). Definition Build_evard_package {s d} (v : s) (vald : d) (evard_package_pfT : s = d) |