diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-10 12:42:45 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-10 13:29:07 -0500 |
| commit | b9fe2a4024280b35b32cc4e532eaa0c820b3b14d (patch) | |
| tree | 1672267456f8d3c3efcd19cbedd88d011fd314e0 /src/Util/SideConditions | |
| parent | ca6b659004aecfbe14448767453ebf9877ff8fbd (diff) | |
Separate case for handling option matches in autosolve
Diffstat (limited to 'src/Util/SideConditions')
| -rw-r--r-- | src/Util/SideConditions/Autosolve.v | 6 |
1 files changed, 5 insertions, 1 deletions
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. |