diff options
Diffstat (limited to 'src/Util/SideConditions')
| -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) |