diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-17 17:29:16 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-17 17:29:16 -0500 |
| commit | ee5e7b6961206a96b9071a1ea2c3d7c1e08e9dac (patch) | |
| tree | af84d4a65ef50a52ed1e8c5a78015b28bdc5369a /src/Util/SideConditions | |
| parent | 4bc5982cc04e19c034cbd8063783538157873b32 (diff) | |
Add fast path for vm_decide (_ = true) package
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 3484891bf..9197ec9d6 100644 --- a/src/Util/SideConditions/ReductionPackages.v +++ b/src/Util/SideConditions/ReductionPackages.v @@ -90,6 +90,7 @@ Ltac autosolve autosolve_tac else_tac := progress change x with x'; cbv beta iota; autosolve_tac else_tac + | [ |- vm_decide_package (_ = true) ] => abstract vm_cast_no_check (eq_refl true) | [ |- 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 |