diff options
-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 |