diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-07 18:48:13 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-07 18:59:04 -0500 |
commit | e9fe0e2cbb98f6b8dcd7c15c7a850bb76f91e8a7 (patch) | |
tree | 9f7fe311c30d8e5d3a6b24157fcb747325a3eb3a /src/Util/SideConditions/Autosolve.v | |
parent | 7b0d663d707f22931dbffb0ce3e803b689884be4 (diff) |
Better way (hopefully) of projecting relation from evar package
Diffstat (limited to 'src/Util/SideConditions/Autosolve.v')
-rw-r--r-- | src/Util/SideConditions/Autosolve.v | 17 |
1 files changed, 6 insertions, 11 deletions
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). |