From f4b9bf1646e0b37541ebde5b030a90f4c762173b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 20:25:30 -0500 Subject: Base evard_package on evar_rel_package --- src/Util/SideConditions/CorePackages.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/Util/SideConditions') 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) -- cgit v1.2.3