Version of `app` for proof mode.

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 {_ _} _ !_ /.

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.