Commit 470c73cf authored by Robbert's avatar Robbert

Merge branch 'ci/janno/reduction_no_check' into 'master'

Avoid conversion after only reducing goal.

See merge request iris/iris!235
parents d5b0ff9a 46e7af84
......@@ -20,7 +20,9 @@ Declare Reduction pm_eval := cbv [
Ltac pm_eval t :=
eval pm_eval in t.
Ltac pm_reduce :=
match goal with |- ?u => let v := pm_eval u in change v end.
(* Use [convert_concl_no_check] instead of [change] to avoid performing the
conversion check twice. *)
match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end.
Ltac pm_reflexivity := pm_reduce; exact eq_refl.
(** Called by many tactics for redexes that are created by instantiation.
......@@ -34,4 +36,6 @@ Declare Reduction pm_prettify := cbn [
bi_tforall bi_texist
].
Ltac pm_prettify :=
match goal with |- ?u => let v := eval pm_prettify in u in change v end.
(* Use [convert_concl_no_check] instead of [change] to avoid performing the
conversion check twice. *)
match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment