Kill warnings in Coq 8.12.

theories/examples/namegen.v

@@ -69,7 +69,7 @@ Section namegen_refinement.
       iAssert (⌜(∃ x, (x, S n) ∈ L) → False⌝)%I with "[HL]" as %Hc.
       { iIntros (Hx). destruct Hx as [x Hy].
         rewrite (big_sepS_elem_of _ L (x,S n) Hy).
-        iDestruct "HL" as "[_ %]". omega. }
+        iDestruct "HL" as "[_ %]". lia. }
       iMod (bij_alloc_alt _ _ γ _ l' (S n) with "HB") as "[HB #Hl'n]"; auto.
       iMod ("Hcl" with "[-]").
       { iNext.

theories/prelude/asubst.v

@@ -11,8 +11,6 @@ Section Autosubst_Lemmas.
     upn m f x = if decide (x < m) then ids x else rename (+m) (f (x - m)).
   Proof.
     revert x; induction m as [|m IH]=> -[|x];
-    repeat (case_match || asimpl || rewrite IH); auto with omega.
-    { exfalso. clear Heqs. revert l. lia. }
-    { exfalso. apply n. lia. }
+      repeat (case_match || asimpl || rewrite IH); auto with lia.
   Qed.
 End Autosubst_Lemmas.

theories/typing/contextual_refinement.v

@@ -53,7 +53,7 @@ Inductive ctx_item :=
   | CTX_UnpackR (x : binder) (e1 : expr)
 .
 
-Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
+Definition fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   match ctx with
   (* Base lambda calculus *)
   | CTX_Rec f x => Rec f x e

theories/typing/types.v

@@ -102,12 +102,10 @@ Definition rec_unfold : val := λ: "x", "x".
 Definition unpack : val := λ: "x" "y", "y" "x".
 
 Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (Lam x%binder e2%E))
-  (at level 200, x at level 1, e1, e2 at level 200, only parsing,
-   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
+  (at level 200, x at level 1, e1, e2 at level 200, only parsing) : expr_scope.
 
 Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (LamV x%binder e2%E))
-  (at level 200, x at level 1, e1, e2 at level 200, only parsing,
-   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : val_scope.
+  (at level 200, x at level 1, e1, e2 at level 200, only parsing) : val_scope.
 
 (** Operation lifts *)
 Instance insert_binder (A : Type): Insert binder A (stringmap A) :=