From ca6b659004aecfbe14448767453ebf9877ff8fbd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Nov 2017 12:34:12 -0500 Subject: Add cbn [val] in autosolve --- src/Util/SideConditions/Autosolve.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/SideConditions') diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v index 9622ba689..05d4ec786 100644 --- a/src/Util/SideConditions/Autosolve.v +++ b/src/Util/SideConditions/Autosolve.v @@ -13,6 +13,7 @@ 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_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. Definition optional_evar_Prop_package {T} (P : T -> Prop) (alt_pkg : Type) := @evar_Prop_package @@ -97,8 +98,14 @@ Ltac autosolve else_tac := => exact (@Build_evard_package s d v v eq_refl eq_refl) + | [ |- vm_compute_cast_evar_package (s:=?s) ?v ?d ] + => let v' := (eval vm_compute in v) in + exact (@Build_evard_package + s d v + v' eq_refl eq_refl) | [ |- @option_evar_rel_package ?A ?v ?B ?R ?alt_pkg ] => refine (@unoption_evar_rel_package A v B R alt_pkg (fun _ x => x) _); + cbn [val]; autosolve else_tac | _ => CorePackages.autosolve else_tac end. -- cgit v1.2.3