From a96f7f9c31713cee36949e7a7e8c52227f301014 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 17 Nov 2017 18:30:32 -0500 Subject: Add fast path for vm_decide (_ = false) --- src/Util/SideConditions/ReductionPackages.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Util/SideConditions') 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 -- cgit v1.2.3