From e9fe0e2cbb98f6b8dcd7c15c7a850bb76f91e8a7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 18:48:13 -0500 Subject: Better way (hopefully) of projecting relation from evar package --- src/Util/SideConditions/Autosolve.v | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'src/Util/SideConditions') diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v index 9b2ce79c1..9622ba689 100644 --- a/src/Util/SideConditions/Autosolve.v +++ b/src/Util/SideConditions/Autosolve.v @@ -41,21 +41,16 @@ Definition option_evar_rel_package {A} (v : option A) B (R : B -> A -> Prop) (al | Some _, None | None, Some _ => False end). -Ltac project_rel_from_evar_rel_package pkg_type := - lazymatch pkg_type with - | evar_rel_package ?v ?B ?R - => R - | ?T - => let h := head_under_binders T in - let pkg_type' := (eval cbv [h] in T) in - project_rel_from_evar_rel_package pkg_type' - end. - Notation optional_evar_rel_package pkg_type x := (option_evar_rel_package x _ - (ltac:(let R := project_rel_from_evar_rel_package pkg_type in exact r)) + (fun a b + => ltac:(lazymatch eval hnf in (pkg_type b) with + | evar_Prop_package ?P + => let P := (eval cbv beta in (P a)) in + exact P + end)) pkg_type) (only parsing). -- cgit v1.2.3