aboutsummaryrefslogtreecommitdiff
path: root/src/Util/SideConditions
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-16 17:17:53 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-16 17:53:52 -0500
commiteeb50337811b46dc52b9b62266b6335d9f90264b (patch)
tree210cff748b2aeabfb0bf31d143fb7fecd66cb4f4 /src/Util/SideConditions
parent4ddbfb44bd91182034ab4f2a548438ab1f8559b6 (diff)
Add vm_compute_cbv_evar_package
Diffstat (limited to 'src/Util/SideConditions')
-rw-r--r--src/Util/SideConditions/ReductionPackages.v13
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/SideConditions/ReductionPackages.v b/src/Util/SideConditions/ReductionPackages.v
index 3266540ac..0bba4811f 100644
--- a/src/Util/SideConditions/ReductionPackages.v
+++ b/src/Util/SideConditions/ReductionPackages.v
@@ -11,6 +11,11 @@ Definition vm_compute_evar_package_gen {bias : cast_bias} {T} (v : T) :=
Notation vm_compute_evar_package_vm_small := (@vm_compute_evar_package_gen LHS).
Notation vm_compute_evar_package_vm_large := (@vm_compute_evar_package_gen RHS).
Notation vm_compute_evar_package := vm_compute_evar_package_vm_small.
+Definition vm_compute_cbv_evar_package_gen {bias : cast_bias} {T} (v : T) :=
+ @evar_package T v.
+Notation vm_compute_cbv_evar_package_vm_small := (@vm_compute_cbv_evar_package_gen LHS).
+Notation vm_compute_cbv_evar_package_vm_large := (@vm_compute_cbv_evar_package_gen RHS).
+Notation vm_compute_cbv_evar_package := vm_compute_cbv_evar_package_vm_small.
Definition vm_cast_evar_package {s} (v : s) d := @evard_package s d v.
Definition cast_evar_package {s} (v : s) d := @evard_package s d v.
Definition vm_compute_cast_evar_package {s} (v : s) d := @evard_package s d v.
@@ -89,6 +94,14 @@ Ltac autosolve autosolve_tac else_tac :=
| [ |- vm_compute_evar_package_vm_large ?v ]
=> let v' := (eval vm_compute in v) in
(exists v'); abstract vm_cast_no_check (eq_refl v)
+ | [ |- vm_compute_cbv_evar_package_vm_small ?v ]
+ => let v' := (eval vm_compute in v) in
+ let v' := (eval cbv in v) in
+ (exists v'); abstract vm_cast_no_check (eq_refl v')
+ | [ |- vm_compute_cbv_evar_package_vm_large ?v ]
+ => let v' := (eval vm_compute in v) in
+ let v' := (eval cbv in v) in
+ (exists v'); abstract vm_cast_no_check (eq_refl v)
| [ |- vm_cast_evar_package ?v ?d ]
=> unshelve eexists (v <: d);
[ vm_compute; reflexivity