remove Pos.succ from proofmode unfold list by making a copy

theories/proofmode/base.v

@@ -8,14 +8,21 @@ Set Default Proof Using "Type".
 (* Directions of rewrites *)
 Inductive direction := Left | Right.
 
-(* Some specific versions of operations on strings for the proof mode. We need
-those so that we can make [cbv] unfold just them, but not the actual operations
-that may appear in users' proofs. *)
+(* Some specific versions of operations on strings, booleans, positive for the
+proof mode. We need those so that we can make [cbv] unfold just them, but not
+the actual operations that may appear in users' proofs. *)
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
 Lemma lazy_andb_true (b1 b2 : bool) : b1 && b2 = true ↔ b1 = true ∧ b2 = true.
 Proof. destruct b1, b2; intuition congruence. Qed.
 
+Fixpoint Pos_succ (x : positive) : positive :=
+  match x with
+  | (p~1)%positive => ((Pos_succ p)~0)%positive
+  | (p~0)%positive => (p~1)%positive
+  | 1%positive => 2%positive
+  end.
+
 Definition beq (b1 b2 : bool) : bool :=
   match b1, b2 with
   | false, false | true, true => true

theories/proofmode/environments.v

@@ -312,7 +312,7 @@ Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
   Envs Enil (env_spatial Δ) (env_counter Δ).
 
 Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos.succ (env_counter Δ)).
+  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
 
 Fixpoint envs_split_go {PROP}
     (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=

theories/proofmode/reduction.v

@@ -4,7 +4,7 @@ From iris.proofmode Require Import base environments.
 Declare Reduction pm_cbv := cbv [
   (* base *)
   pm_option_bind pm_from_option pm_option_fun
-  base.beq base.ascii_beq base.string_beq base.positive_beq base.ident_beq
+  base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
   env_lookup env_lookup_delete env_delete env_app env_replace
   env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
@@ -12,9 +12,6 @@ Declare Reduction pm_cbv := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_persistent envs_incr_counter
   envs_split_go envs_split prop_of_env
-  (* other modules. TODO: we should probably make copies of these,
-     but what will that break? *)
-  Pos.succ
 ].
 Ltac pm_eval t :=
   let u := eval pm_cbv in t in