Commit 46e7af84 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add comments.

parent 1595e35f
Pipeline #16333 passed with stage
in 12 minutes and 36 seconds
...@@ -20,6 +20,8 @@ Declare Reduction pm_eval := cbv [ ...@@ -20,6 +20,8 @@ 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 :=
(* 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. 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.
...@@ -34,4 +36,6 @@ Declare Reduction pm_prettify := cbn [ ...@@ -34,4 +36,6 @@ Declare Reduction pm_prettify := cbn [
bi_tforall bi_texist bi_tforall bi_texist
]. ].
Ltac pm_prettify := Ltac pm_prettify :=
(* 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. match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end.
Supports Markdown
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