From eeb50337811b46dc52b9b62266b6335d9f90264b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 16 Nov 2017 17:17:53 -0500 Subject: Add vm_compute_cbv_evar_package --- src/Util/SideConditions/ReductionPackages.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/Util/SideConditions') 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 -- cgit v1.2.3