Merge branch 'robbert/issue259' into 'master'

Fix issue #259: Error message when iRevert is used on out of scope variable

Closes #259

See merge request iris/iris!301

tests/proofmode.ref

@@ -668,3 +668,41 @@ In nested Ltac calls to "iApply (open_constr)",
 failed.
 Tactic failure: iApply: Q
 not absorbing and the remaining hypotheses not affine.
+"iRevert_wrong_var"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) )" and 
+"iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k1 not in scope.
+The command has indeed failed with message:
+In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
+"iLöbRevert (constr) with (tactic3)",
+"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
+"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
+"∗" with tac), "iRevertIntros (constr) with (tactic3)", 
+"iRevertIntros_go", "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as
+IH), "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
+"iRevertIntros ( (ident) ) (constr) with (tactic3)",
+"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
+"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )), 
+"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
+"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k1 not in scope.
+"iRevert_dup_var"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) (ident) )",
+"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k not in scope.
+"iRevert_dep_var_coq"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) )", "iForallRevert (ident)" and
+"revert (ne_var_list)", last call failed.
+k is used in hypothesis Hk.
+"iRevert_dep_var"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iRevert ( (ident) )" and 
+"iForallRevert (ident)", last call failed.
+Tactic failure: iRevert: k is used in hypothesis "Hk".

tests/proofmode.v

@@ -684,7 +684,6 @@ Lemma test_iDestruct_clear P Q R :
 Proof.
   iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
 Qed.
-
 End tests.
 
 (** Test specifically if certain things print correctly. *)
@@ -909,4 +908,23 @@ Proof. iIntros "HP HQ". Fail iApply "HQ". Abort.
 Check "iApply_fail_not_affine_2".
 Lemma iApply_fail_not_affine_1 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
 Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
+
+Check "iRevert_wrong_var".
+Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : Φ (S k).
+Proof.
+  Fail iRevert (k1).
+  Fail iLöb as "IH" forall (k1).
+Abort.
+
+Check "iRevert_dup_var".
+Lemma iRevert_dup_var (k : nat) (Φ : nat → PROP) : Φ (S k).
+Proof. Fail iRevert (k k). Abort.
+
+Check "iRevert_dep_var_coq".
+Lemma iRevert_dep_var_coq (k : nat) (Φ : nat → PROP) : k = 0 → Φ (S k).
+Proof. intros Hk. Fail iRevert (k). Abort.
+
+Check "iRevert_dep_var".
+Lemma iRevert_dep_var (k : nat) (Φ : nat → PROP) : Φ k -∗ Φ (S k).
+Proof. iIntros "Hk". Fail iRevert (k). Abort.
 End error_tests.

theories/proofmode/ltac_tactics.v

@@ -570,9 +570,11 @@ Local Tactic Notation "iForallRevert" ident(x) :=
     intros x;
     iMatchHyp (fun H P =>
       lazymatch P with
-      | context [x] => fail 2 "iRevert:" x "is used in hypothesis" H
+      | context [x] =>
+         let H := pretty_ident H in fail 2 "iRevert:" x "is used in hypothesis" H
       end) in
   iStartProof;
+  first [let _ := type of x in idtac|fail 1 "iRevert:" x "not in scope"];
   let A := type of x in
   lazymatch type of A with
   | Prop => revert x; first [apply tac_pure_revert|err x]
@@ -1746,14 +1748,15 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
   iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x15 ); iIntros p2.
 
 (* Used for generalization in iInduction and iLöb *)
+Ltac iRevertIntros_go Hs tac :=
+  lazymatch Hs with
+  | [] => tac
+  | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
+  | ESelIdent ?p ?H :: ?Hs => iRevertHyp H; iRevertIntros_go Hs tac; iIntro H as p
+  end.
+
 Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
-  let rec go Hs :=
-    lazymatch Hs with
-    | [] => tac
-    | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
-    | ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
-    end in
-  try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
+  try iStartProof; let Hs := iElaborateSelPat Hs in iRevertIntros_go Hs tac.
 
 Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1); tac; iIntros (x1)).