Base evard_package on evar_rel_package

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)