Skip to content
Snippets Groups Projects
Commit f4655145 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

A tweak suggested by @janno that may improve performance.

parent d5b0ff9a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/reduction.v
+ 1
− 1
View file @ f4655145
...@@ -20,7 +20,7 @@ Declare Reduction pm_eval := cbv [ ...@@ -20,7 +20,7 @@ Declare Reduction pm_eval := cbv [
Ltac pm_eval t := Ltac pm_eval t :=
eval pm_eval in t. eval pm_eval in t.
Ltac pm_reduce := Ltac pm_reduce :=
match goal with |- ?u => let v := pm_eval u in change v end. match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end.
Ltac pm_reflexivity := pm_reduce; exact eq_refl. Ltac pm_reflexivity := pm_reduce; exact eq_refl.
(** Called by many tactics for redexes that are created by instantiation. (** Called by many tactics for redexes that are created by instantiation.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment