Tests.

tests/proofmode.ref

@@ -723,6 +723,52 @@ No applicable tactic.
   "H" : ⌜φ⌝ -∗ P
   --------------------------------------∗
   ⌜φ⌝ -∗ P
+"test_iInduction_revert_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  n : nat
+  P : nat → PROP
+  Hn : 0 < S n
+  ============================
+  "IH" : <affine> ⌜0 < n⌝ -∗ P n
+  --------------------------------------□
+  P (S n)
+1 goal
+  
+  PROP : bi
+  n : nat
+  Hn : 0 < S n
+  P : nat → PROP
+  ============================
+  "IH" : <affine> ⌜0 < n⌝ -∗ P n
+  --------------------------------------□
+  P (S n)
+"test_iInduction_revert_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  n : nat
+  P : nat → PROP
+  Hn : 0 < S n
+  ============================
+  "IH" : ⌜0 < n⌝ -∗ P n
+  --------------------------------------□
+  P (S n)
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  n : nat
+  Hn : 0 < S n
+  P : nat → PROP
+  ============================
+  "IH" : ⌜0 < n⌝ -∗ P n
+  --------------------------------------□
+  P (S n)
 "test_iFrame_not_add_emp_for_intuitionistically"
      : string
 1 goal

tests/proofmode.v

@@ -1602,6 +1602,32 @@ Proof.
   iIntros (Hφ) "H". iRevert (Hφ). Show. done.
 Qed.
 
+Check "test_iInduction_revert_pure".
+Lemma test_iInduction_revert_pure (n : nat) (Hn : 0 < n) (P : nat → PROP) :
+  ⊢ P n.
+Proof.
+  (* Check that we consistently get [<affine> _ -∗], not [→] *)
+  iInduction n as [|n] "IH" forall (Hn); first lia.
+  Show.
+Restart.
+Proof.
+  iInduction n as [|n] "IH"; first lia.
+  Show.
+Abort.
+
+Check "test_iInduction_revert_pure_affine".
+Lemma test_iInduction_revert_pure_affine `{!BiAffine PROP}
+  (n : nat) (Hn : 0 < n) (P : nat → PROP) : ⊢ P n.
+Proof.
+  (* Check that we consistently get [-∗], not [→]; and no [<affine>] *)
+  iInduction n as [|n] "IH" forall (Hn); first lia.
+  Show.
+Restart.
+Proof.
+  iInduction n as [|n] "IH"; first lia.
+  Show.
+Abort.
+
 (* Check that when framing things under the □ modality, we do not add [emp] in
 affine BIs. *)
 Check "test_iFrame_not_add_emp_for_intuitionistically".