diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-17 18:30:32 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-17 18:30:46 -0500 |
| commit | a96f7f9c31713cee36949e7a7e8c52227f301014 (patch) | |
| tree | b3940b9c85e69a8e3b3ae1556c99e1b2342f5177 /src/Util/SideConditions | |
| parent | d70467b566eedb611bf0574bb30c654f0538b1e4 (diff) | |
Add fast path for vm_decide (_ = false)
Diffstat (limited to 'src/Util/SideConditions')
| -rw-r--r-- | src/Util/SideConditions/ReductionPackages.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/SideConditions/ReductionPackages.v b/src/Util/SideConditions/ReductionPackages.v index 9197ec9d6..980dc4103 100644 --- a/src/Util/SideConditions/ReductionPackages.v +++ b/src/Util/SideConditions/ReductionPackages.v @@ -91,6 +91,7 @@ Ltac autosolve autosolve_tac else_tac := cbv beta iota; autosolve_tac else_tac | [ |- vm_decide_package (_ = true) ] => abstract vm_cast_no_check (eq_refl true) + | [ |- vm_decide_package (_ = false) ] => abstract vm_cast_no_check (eq_refl false) | [ |- 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 |