From 5c959e86cbb684d6507e40651693aeb1b4cc0b80 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jul 2018 14:37:17 +0200
Subject: [PATCH] rename Declare Reduction to match the tactics
---
theories/proofmode/reduction.v | 32 ++++++++++++++------------------
1 file changed, 14 insertions(+), 18 deletions(-)
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 485aacfbc..d13067c9b 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -1,7 +1,10 @@
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import base environments.
-Declare Reduction pm_cbv := cbv [
+(** Called by all tactics to perform computation to lookup items in the
+ context. We avoid reducing anything user-visible here to make sure we
+ do not reduce e.g. before unification happens in [iApply].*)
+Declare Reduction pm_eval := cbv [
(* base *)
base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
(* environments *)
@@ -14,28 +17,21 @@ Declare Reduction pm_cbv := cbv [
(* PM option combinators *)
pm_option_bind pm_from_option pm_option_fun
].
-(* Some things should only be unfolded according to cbn rules, when
- certain arguments are constructors. This is because they can appear in
- the user side of proofs as well. *)
-Declare Reduction pm_cbn := cbn [
- (* telescope combinators *)
- tele_fold tele_bind tele_app
- (* BI connectives *)
- bi_persistently_if bi_affinely_if bi_intuitionistically_if
- bi_wandM sbi_laterN
- bi_tforall bi_texist
-].
-
-(** Called by all tactics to perform computation to lookup items in the
- context. We avoid reducing anything user-visible here to make sure we
- do not reduce e.g. before unification happens in [iApply].*)
Ltac pm_eval t :=
- eval pm_cbv in t.
+ eval pm_eval in t.
Ltac pm_reduce :=
match goal with |- ?u => let v := pm_eval u in change v end.
Ltac pm_reflexivity := pm_reduce; exact eq_refl.
(** Called by many tactics for redexes that are created by instantiation.
This cannot create any envs redexes so we just do the cbn part. *)
+Declare Reduction pm_prettify := cbn [
+ (* telescope combinators *)
+ tele_fold tele_bind tele_app
+ (* BI connectives *)
+ bi_persistently_if bi_affinely_if bi_intuitionistically_if
+ bi_wandM sbi_laterN
+ bi_tforall bi_texist
+].
Ltac pm_prettify :=
- match goal with |- ?u => let v := eval pm_cbn in u in change v end.
+ match goal with |- ?u => let v := eval pm_prettify in u in change v end.
--
GitLab