Adapt to rocq-prover/rocq#20855

Author: proux01

test-suite/output/NotationsCoercionsString.v

@@ -12,7 +12,7 @@ Inductive expr :=
   | Lam : string -> expr -> expr
   | App : expr -> expr -> expr.
 
-Notation Let x e1 e2 := (App (Lam x e2) e1).
+Abbreviation Let x e1 e2 := (App (Lam x e2) e1).
 Parameter e1 e2 : expr.
 Check (Let "x" e1 e2). (* always printed the same *)
 Coercion App : expr >-> Funclass.

test-suite/output/StringSyntax.v

@@ -54,7 +54,7 @@ Compute List.map Ascii.ascii_of_nat (ListDef.seq 0 256).
 (* Test numeral notations for parameterized inductives *)
 Module Test2.
 
-Notation string := (list Byte.byte).
+Abbreviation string := (list Byte.byte).
 Definition id_string := @id string.
 
 String Notation string id_string id_string : list_scope.
@@ -99,12 +99,12 @@ End Test3.
 (* Test overlapping string notations *)
 Module Test4.
 
-Notation string1 := (list Byte.byte).
+Abbreviation string1 := (list Byte.byte).
 Definition id_string1 := @id string1.
 
 String Notation string1 id_string1 id_string1 : list_scope.
 
-Notation string2 := (list Ascii.ascii).
+Abbreviation string2 := (list Ascii.ascii).
 Definition a2b := List.map byte_of_ascii.
 Definition b2a := List.map ascii_of_byte.
 

test-suite/output/simpl.v

@@ -44,7 +44,7 @@ Check "** NonPrimitiveProjection".
 Module DirectTuple.
 Check "DirectTuple (NonPrimitiveProjection)".
 Record T := {p:nat}.
-Notation TUPLE := {|p:=0|}.
+Abbreviation TUPLE := {|p:=0|}.
 Eval simpl in TUPLE.(p).  (* -> 0 *)
 Eval cbn in TUPLE.(p).    (* -> 0 *)
 Eval hnf in TUPLE.(p).    (* -> 0 *)
@@ -76,7 +76,7 @@ End NamedTuple.
 Module DirectCoFix.
 Check "DirectCoFix (NonPrimitiveProjection)".
 CoInductive U := {p:U}.
-Notation COFIX := (cofix a := {|p:=a|}).
+Abbreviation COFIX := (cofix a := {|p:=a|}).
 Eval simpl in COFIX.(p).  (* -> COFIX *)
 Eval cbn in COFIX.(p).    (* -> COFIX *)
 Eval hnf in COFIX.(p).    (* -> COFIX *)
@@ -112,7 +112,7 @@ Set Primitive Projections.
 Module DirectTuple.
 Check "DirectTuple (PrimitiveProjectionFolded)".
 Record T := {p:nat}.
-Notation TUPLE := {|p:=0|}.
+Abbreviation TUPLE := {|p:=0|}.
 Eval simpl in TUPLE.(p).  (* -> 0 *)
 Eval cbn in TUPLE.(p).    (* -> 0 *)
 Eval hnf in TUPLE.(p).    (* -> 0 *)
@@ -143,7 +143,7 @@ End NamedTuple.
 Module DirectCoFix.
 Check "DirectCoFix (PrimitiveProjectionFolded)".
 CoInductive U := {p:U}.
-Notation COFIX := (cofix a := {|p:=a|}).
+Abbreviation COFIX := (cofix a := {|p:=a|}).
 Eval simpl in COFIX.(p).  (* -> COFIX *)
 Eval cbn in COFIX.(p).    (* -> COFIX *)
 Eval hnf in COFIX.(p).    (* -> COFIX *)
@@ -214,7 +214,7 @@ Module DirectCoFix.
 Check "DirectCoFix (PrimitiveProjectionUnfolded)".
 CoInductive U := {q:U}.
 CoFixpoint a := {|q:=a|}.
-Notation COFIX := (cofix a := {|q:=a|}).
+Abbreviation COFIX := (cofix a := {|q:=a|}).
 Axiom P : U -> Prop.
 Goal P a.(q). unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *)
 Goal P a.(q). unfold q. cbv delta [a]. cbn. Show. Abort.   (* -> COFIX *)
@@ -229,7 +229,7 @@ Module NamedCoFix.
 Check "NamedCoFix (PrimitiveProjectionUnfolded)".
 CoInductive U := {q:U}.
 CoFixpoint a := {|q:=a|}.
-Notation COFIX := (cofix a := {|q:=a|}).
+Abbreviation COFIX := (cofix a := {|q:=a|}).
 Axiom P : U -> Prop.
 Goal P a.(q). unfold q. simpl. Show. Abort.  (* -> a *)
 Goal P a.(q). unfold q. cbn. Show. Abort.    (* -> a *)
@@ -254,7 +254,7 @@ Set Primitive Projections.
 Module DirectTuple.
 Check "DirectTuple (PrimitiveProjectionConstant)".
 Record T := {p:nat}.
-Notation TUPLE := {|p:=0|}.
+Abbreviation TUPLE := {|p:=0|}.
 Definition a := {|p:=0|}.
 Axiom P : nat -> Prop.
 Goal P (id p a). unfold id. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
@@ -288,7 +288,7 @@ End NamedTuple.
 Module DirectCoFix.
 Check "DirectCoFix (PrimitiveProjectionConstant)".
 CoInductive U := {q:U}.
-Notation COFIX := (cofix a := {|q:=a|}).
+Abbreviation COFIX := (cofix a := {|q:=a|}).
 Axiom P : U -> Prop.
 Goal P (id q COFIX). unfold id. simpl. Show. Abort.  (* -> COFIX *)
 Goal P (id q COFIX). unfold id. cbn. Show. Abort.    (* -> COFIX *)

theories/_CoqProject

@@ -1 +1,4 @@
 -R . Stdlib
+# to handle when requiring Rocq >= 9.2
+-arg -w -arg -notation-for-abbreviation
+-arg -w -arg -ltac2-notation-for-abbreviation

theories/dune

@@ -6,7 +6,8 @@
 (env
  (dev
   (coq
-   (flags :standard))))
+   ;; see theories/_CoqProject for details
+   (flags :standard -w -notation-for-abbreviation -w -ltac2-notation-for-abbreviation))))
 
 (rule
  (targets All.v)