From b9fe2a4024280b35b32cc4e532eaa0c820b3b14d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Nov 2017 12:42:45 -0500 Subject: Separate case for handling option matches in autosolve --- src/Util/SideConditions/Autosolve.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/Util/SideConditions') diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v index 05d4ec786..3428a77e9 100644 --- a/src/Util/SideConditions/Autosolve.v +++ b/src/Util/SideConditions/Autosolve.v @@ -79,6 +79,11 @@ Ltac autosolve else_tac := | [ |- True ] => exact I | [ |- unit ] => exact tt | [ |- IDProp ] => exact idProp + | [ |- match ?x with Some _ => _ | None => _ end ] + => let x' := (eval hnf in x) in + progress change x with x'; + cbv beta iota; + autosolve else_tac | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity @@ -105,7 +110,6 @@ Ltac autosolve else_tac := 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