make 'oinv 1' work

stdpp/tactics.v

@@ -700,6 +700,21 @@ Tactic Notation "oinv" uconstr(p) :=
     else
       let Hp := fresh in pose proof p as Hp; inv Hp).
 
+(* As above, we overload the notation with [integer] and [ident] to support
+[oinv 1], like the regular [inversion] tactic. *)
+Tactic Notation "oinv" integer(n) "as" simple_intropattern(ipat) :=
+  intros until n;
+  lazymatch goal with
+  | H : _ |- _ => (* matches the last hypothesis, which is what we want *)
+      oinv H as ipat
+  end.
+Tactic Notation "oinv" integer(n) :=
+  intros until n;
+  lazymatch goal with
+  | H : _ |- _ => (* matches the last hypothesis, which is what we want *)
+      oinv H
+  end.
+
 (** Helper for [ospecialize]: call [tac] with the name of the head term *if*
 that term is a variable.
 

tests/tactics.ref

@@ -51,10 +51,16 @@ use opose proof instead.
   EQ : n' = n
   ============================
   even n
-"oinv_test1"
+"oinv_test2"
      : string
 1 goal
   
+  n : nat
+  H' : even n
+  ============================
+  even n
+1 goal
+  
   n : nat
   H' : even n
   ============================

tests/tactics.v

@@ -197,9 +197,20 @@ Proof. intros H. oinversion H as [|n' Hn' EQ]. Show. done. Qed.
 Lemma oinv_test1 : ~(∀ n, even n).
 Proof. intros H. oinv (H 1). Qed.
 (* Ensure we clear the [H] if appropriate. *)
-Check "oinv_test1".
+Check "oinv_test2".
 Lemma oinv_test2 n : even (2 + n) → even n.
-Proof. intros H. oinv H as [|? H']. Show. done. Qed.
+Proof.
+  intros H. oinv H as [|? H']. Show. done.
+Restart.
+  oinv 1 as [|? H']. Show. done.
+Qed.
+Lemma oinv_test_num (P : Prop) n :
+  P → (P → even (2 + n)) → even n.
+Proof.
+  intros HP. oinv 1.
+  { exact HP. }
+  done.
+Qed.
 
 (** Some tests for f_equiv. *)
 (* Similar to [f_equal], it should solve goals by [reflexivity]. *)