diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-07 15:22:40 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-07 15:24:59 -0500 |
| commit | c510453583a780ab225bdd53cda3cdd4d9d2d397 (patch) | |
| tree | e8d2a32e569ca90dc4a651a155077bed3f3c4f86 /src/Util/SideConditions/Autosolve.v | |
| parent | ae96b60dc9264703ed6a43c48e0c4892bffad131 (diff) | |
Factor packages through evar_Prop_package, raw_evar_package
Diffstat (limited to 'src/Util/SideConditions/Autosolve.v')
| -rw-r--r-- | src/Util/SideConditions/Autosolve.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v index 7bc47def3..90c317742 100644 --- a/src/Util/SideConditions/Autosolve.v +++ b/src/Util/SideConditions/Autosolve.v @@ -26,9 +26,10 @@ Module Internal. => let v' := (eval vm_compute in v) in (exists v'); abstract vm_cast_no_check (eq_refl v) | [ |- vm_cast_evar_package ?v ?d ] - => simple refine {| vald := (v <: d) |}; + => unshelve eexists (v <: d); [ vm_compute; reflexivity - | let lhs := lazymatch goal with |- ?lhs = _ => lhs end in + | cbv beta; + let lhs := lazymatch goal with |- ?lhs = _ => lhs end in abstract exact_no_check (eq_refl lhs) ] | [ |- cast_evar_package (s:=?s) ?v ?d ] => exact (@Build_evard_package |