From c7842c944223e7618e6b6aae784d110229b9130a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Dec 2019 23:41:08 +0100
Subject: [PATCH] Version of `app` for proof mode.

---
 theories/proofmode/base.v      | 5 ++++-
 theories/proofmode/reduction.v | 4 ++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index bc251fe25..e50c8c88d 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -98,7 +98,10 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
 
-(** Copies of some [option] combinators for better reduction control. *)
+(** Copies of some functions on [list] and [option] for better reduction control. *)
+Fixpoint pm_app {A} (l1 l2 : list A) : list A :=
+  match l1 with [] => l2 | x :: l1 => x :: pm_app l1 l2 end.
+
 Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B :=
   match mx with Some x => f x | None => None end.
 Arguments pm_option_bind {_ _} _ !_ /.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 0cfc07623..6ce3ffd9c 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -16,8 +16,8 @@ Declare Reduction pm_eval := cbv [
   envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
   envs_split_go envs_split
   env_to_prop_go env_to_prop env_to_prop_and_go env_to_prop_and
-  (* PM option combinators *)
-  pm_option_bind pm_from_option pm_option_fun
+  (* PM list and option functions *)
+  pm_app pm_option_bind pm_from_option pm_option_fun
 ].
 Ltac pm_eval t :=
   eval pm_eval in t.
-- 
GitLab