From c6a6c8b89e987004aee9a86dcb4881e734727719 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 30 Oct 2023 16:30:14 +0100
Subject: [PATCH 1/3] Move reservation of notations .1 and .2 from ssr to Init

Also move them from level 2 to level 1 in preparation
of removal of camlp5 recovery mechanism.
---
 test-suite/bugs/HoTT_coq_058.v      | 2 +-
 test-suite/bugs/bug_3317.v          | 8 ++++----
 test-suite/bugs/bug_3446.v          | 4 ++--
 test-suite/bugs/bug_3480.v          | 2 +-
 test-suite/bugs/bug_3485.v          | 4 ++--
 test-suite/bugs/bug_3640.v          | 4 ++--
 test-suite/bugs/bug_3668.v          | 2 +-
 test-suite/bugs/bug_3698.v          | 2 +-
 test-suite/bugs/bug_3699.v          | 8 ++++----
 test-suite/bugs/bug_3710.v          | 2 +-
 test-suite/bugs/bug_3754.v          | 2 +-
 test-suite/bugs/bug_4089.v          | 4 ++--
 test-suite/bugs/bug_4097.v          | 4 ++--
 test-suite/bugs/bug_4116.v          | 4 ++--
 test-suite/bugs/bug_4527.v          | 4 ++--
 test-suite/bugs/bug_4533.v          | 4 ++--
 test-suite/bugs/bug_4544.v          | 4 ++--
 test-suite/bugs/bug_4634.v          | 4 ++--
 test-suite/bugs/bug_4780.v          | 4 ++--
 test-suite/bugs/bug_7059.v          | 4 ++--
 test-suite/output/PrintGrammar.out  | 4 +++-
 test-suite/output/PrintKeywords.out | 2 ++
 test-suite/success/eauto.v          | 8 ++++----
 theories/Init/Notations.v           | 5 +++++
 theories/ssr/ssrfun.v               | 2 --
 25 files changed, 52 insertions(+), 45 deletions(-)

diff --git a/test-suite/bugs/HoTT_coq_058.v b/test-suite/bugs/HoTT_coq_058.v
index 09e4365ebe3c..1c9f7caf25f2 100644
--- a/test-suite/bugs/HoTT_coq_058.v
+++ b/test-suite/bugs/HoTT_coq_058.v
@@ -4,7 +4,7 @@ Set Universe Polymorphism.
 Notation idmap := (fun x => x).
 Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Open Scope fibration_scope.
-Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
+Notation "x .1" := (projT1 x) : fibration_scope.
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a.
 Arguments idpath {A a} , [A] a.
diff --git a/test-suite/bugs/bug_3317.v b/test-suite/bugs/bug_3317.v
index 74199166459c..d175b8165f9e 100644
--- a/test-suite/bugs/bug_3317.v
+++ b/test-suite/bugs/bug_3317.v
@@ -9,8 +9,8 @@ Module A.
   Arguments existT {A} _ _ _.
   Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
     match p with idpath => u end.
-  Notation "x .1" := (projT1 x) (at level 3).
-  Notation "x .2" := (projT2 x) (at level 3).
+  Notation "x .1" := (projT1 x).
+  Notation "x .2" := (projT2 x).
   Notation "( x ; y )" := (existT _ x y).
   Set Printing All.
   Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
@@ -64,8 +64,8 @@ Module B.
   Arguments existT {A} _ _ _.
   Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
     match p with idpath => u end.
-  Notation "x .1" := (projT1 x) (at level 3).
-  Notation "x .2" := (projT2 x) (at level 3).
+  Notation "x .1" := (projT1 x).
+  Notation "x .2" := (projT2 x).
   Notation "( x ; y )" := (existT _ x y).
   Set Printing All.
 
diff --git a/test-suite/bugs/bug_3446.v b/test-suite/bugs/bug_3446.v
index c115a44e1079..9a4d365ed491 100644
--- a/test-suite/bugs/bug_3446.v
+++ b/test-suite/bugs/bug_3446.v
@@ -33,8 +33,8 @@ Set Universe Polymorphism.
 Arguments projT1 {_ _} _.
 Notation "( x ; y )" := (existT _ x y).
 Notation pr1 := projT1.
-Notation "x .1" := (projT1 x) (at level 3).
-Notation "x .2" := (projT2 x) (at level 3).
+Notation "x .1" := (projT1 x).
+Notation "x .2" := (projT2 x).
 Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
 Notation "g 'o' f" := (compose g f) (at level 40, left associativity).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
diff --git a/test-suite/bugs/bug_3480.v b/test-suite/bugs/bug_3480.v
index fd98232f9653..81d8e87b4486 100644
--- a/test-suite/bugs/bug_3480.v
+++ b/test-suite/bugs/bug_3480.v
@@ -3,7 +3,7 @@ Set Primitive Projections.
 Axiom admit : forall {T}, T.
 Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Open Scope fibration_scope.
-Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
+Notation "x .1" := (projT1 x) : fibration_scope.
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
 Set Implicit Arguments.
 Delimit Scope category_scope with category.
diff --git a/test-suite/bugs/bug_3485.v b/test-suite/bugs/bug_3485.v
index 275266410ed3..1bf6812f5d04 100644
--- a/test-suite/bugs/bug_3485.v
+++ b/test-suite/bugs/bug_3485.v
@@ -11,8 +11,8 @@ Tactic Notation "etransitivity" open_constr(y) :=
 Tactic Notation "etransitivity" := etransitivity _.
 Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Open Scope fibration_scope.
-Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
-Notation "x .2" := (projT2 x) (at level 3) : fibration_scope.
+Notation "x .1" := (projT1 x) : fibration_scope.
+Notation "x .2" := (projT2 x) : fibration_scope.
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
 Arguments idpath {A a} , [A] a.
 Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
diff --git a/test-suite/bugs/bug_3640.v b/test-suite/bugs/bug_3640.v
index d0d634bea54b..f482ec614c83 100644
--- a/test-suite/bugs/bug_3640.v
+++ b/test-suite/bugs/bug_3640.v
@@ -5,8 +5,8 @@ Set Primitive Projections.
 Set Implicit Arguments.
 Record sigT {A} P := existT { pr1 : A ; pr2 : P pr1 }.
 Notation "{ x : A & P }" := (sigT (A := A) (fun x : A => P)) : type_scope.
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'").
-Notation "x .2" := (pr2 x) (at level 3, format "x '.2'").
+Notation "x .1" := (pr1 x).
+Notation "x .2" := (pr2 x).
 Record Equiv A B := { equiv_fun :> A -> B }.
 Notation "A <~> B" := (Equiv A B) (at level 85).
 Inductive Bool : Type := true | false.
diff --git a/test-suite/bugs/bug_3668.v b/test-suite/bugs/bug_3668.v
index 3ce37d4f8512..aed867722038 100644
--- a/test-suite/bugs/bug_3668.v
+++ b/test-suite/bugs/bug_3668.v
@@ -4,7 +4,7 @@ Require Import TestSuite.admit.
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
 
 Notation "( x ; y )" := (existT _ x y).
-Notation "x .1" := (projT1 x) (at level 3, format "x '.1'").
+Notation "x .1" := (projT1 x).
 Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
 Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
 Notation "A <~> B" := (Equiv A B) (at level 85).
diff --git a/test-suite/bugs/bug_3698.v b/test-suite/bugs/bug_3698.v
index 21978b710840..bbef18bc8a01 100644
--- a/test-suite/bugs/bug_3698.v
+++ b/test-suite/bugs/bug_3698.v
@@ -6,7 +6,7 @@ Set Primitive Projections.
 Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Open Scope fibration_scope.
 Notation pr1 := projT1.
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
 Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
 Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
 Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
diff --git a/test-suite/bugs/bug_3699.v b/test-suite/bugs/bug_3699.v
index dbb10f94f2f5..9d6e27ed4dfa 100644
--- a/test-suite/bugs/bug_3699.v
+++ b/test-suite/bugs/bug_3699.v
@@ -18,8 +18,8 @@ Module NonPrim.
   Open Scope fibration_scope.
   Notation pr1 := projT1.
   Notation pr2 := projT2.
-  Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-  Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+  Notation "x .1" := (pr1 x) : fibration_scope.
+  Notation "x .2" := (pr2 x) : fibration_scope.
   Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
   Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
   Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
@@ -93,8 +93,8 @@ Module Prim.
   Open Scope fibration_scope.
   Notation pr1 := projT1.
   Notation pr2 := projT2.
-  Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-  Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+  Notation "x .1" := (pr1 x) : fibration_scope.
+  Notation "x .2" := (pr2 x) : fibration_scope.
   Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
   Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
   Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
diff --git a/test-suite/bugs/bug_3710.v b/test-suite/bugs/bug_3710.v
index 07208ffa87b2..0786f3d7f0e4 100644
--- a/test-suite/bugs/bug_3710.v
+++ b/test-suite/bugs/bug_3710.v
@@ -11,7 +11,7 @@ Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope.
 Definition relation (A : Type) := A -> A -> Type.
 Class Reflexive {A} (R : relation A) := reflexivity : forall x : A, R x x.
 Notation "( x ; y )" := (existT _ x y).
-Notation "x .1" := (projT1 x) (at level 3, format "x '.1'").
+Notation "x .1" := (projT1 x).
 Reserved Infix "o" (at level 40, left associativity).
 Delimit Scope category_scope with category.
 Record PreCategory :=
diff --git a/test-suite/bugs/bug_3754.v b/test-suite/bugs/bug_3754.v
index 7031cbf132bb..46450497579a 100644
--- a/test-suite/bugs/bug_3754.v
+++ b/test-suite/bugs/bug_3754.v
@@ -13,7 +13,7 @@ Open Scope fibration_scope.
 
 Notation pr1 := projT1.
 
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
 
 Definition compose {A B C : Type} (g : B -> C) (f : A -> B) :=
   fun x => g (f x).
diff --git a/test-suite/bugs/bug_4089.v b/test-suite/bugs/bug_4089.v
index 69fc4b6a4c2c..0aea11366647 100644
--- a/test-suite/bugs/bug_4089.v
+++ b/test-suite/bugs/bug_4089.v
@@ -85,8 +85,8 @@ Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
 
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 
 Notation compose := (fun g f x => g (f x)).
 
diff --git a/test-suite/bugs/bug_4097.v b/test-suite/bugs/bug_4097.v
index 183b860d1f2d..d4f07b4ee263 100644
--- a/test-suite/bugs/bug_4097.v
+++ b/test-suite/bugs/bug_4097.v
@@ -14,8 +14,8 @@ Open Scope fibration_scope.
 Notation "( x ; y )" := (exist _ _ x y) : fibration_scope.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
 Arguments idpath {A a} , [A] a.
 Notation "x = y :> A" := (@paths A x y) : type_scope.
diff --git a/test-suite/bugs/bug_4116.v b/test-suite/bugs/bug_4116.v
index 7a2eaf72b4f4..d44622f7fe0c 100644
--- a/test-suite/bugs/bug_4116.v
+++ b/test-suite/bugs/bug_4116.v
@@ -29,8 +29,8 @@ Open Scope function_scope.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
 
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 
 Notation compose := (fun g f x => g (f x)).
 
diff --git a/test-suite/bugs/bug_4527.v b/test-suite/bugs/bug_4527.v
index ee5d8fb53d17..f97964e0cc36 100644
--- a/test-suite/bugs/bug_4527.v
+++ b/test-suite/bugs/bug_4527.v
@@ -69,8 +69,8 @@ Open Scope function_scope.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
 
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 
 Notation compose := (fun g f x => g (f x)).
 
diff --git a/test-suite/bugs/bug_4533.v b/test-suite/bugs/bug_4533.v
index 5519f580d19f..bfe65b7747c7 100644
--- a/test-suite/bugs/bug_4533.v
+++ b/test-suite/bugs/bug_4533.v
@@ -51,8 +51,8 @@ Open Scope fibration_scope.
 Open Scope function_scope.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 Notation compose := (fun g f x => g (f x)).
 Notation "g 'o' f" := (compose g%function f%function) (at level 40, left
 associativity) : function_scope.
diff --git a/test-suite/bugs/bug_4544.v b/test-suite/bugs/bug_4544.v
index 29817328f891..4c06c6e17e7c 100644
--- a/test-suite/bugs/bug_4544.v
+++ b/test-suite/bugs/bug_4544.v
@@ -77,8 +77,8 @@ Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
 
-Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
-Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Notation "x .1" := (pr1 x) : fibration_scope.
+Notation "x .2" := (pr2 x) : fibration_scope.
 
 Notation compose := (fun g f x => g (f x)).
 
diff --git a/test-suite/bugs/bug_4634.v b/test-suite/bugs/bug_4634.v
index 77e31e108f29..2f5cfba57644 100644
--- a/test-suite/bugs/bug_4634.v
+++ b/test-suite/bugs/bug_4634.v
@@ -4,8 +4,8 @@ Polymorphic Record pair {A B : Type} : Type :=
   prod { pr1 : A; pr2 : B }.
 
 Notation " ( x ; y ) " := (@prod _ _ x y).
-Notation " x .1 " := (pr1 x) (at level 3).
-Notation " x .2 " := (pr2 x) (at level 3).
+Notation " x .1 " := (pr1 x).
+Notation " x .2 " := (pr2 x).
 
 Goal ((0; 1); 2).1.2 = 1.
 Proof.
diff --git a/test-suite/bugs/bug_4780.v b/test-suite/bugs/bug_4780.v
index c3c277c4e721..54f1d68b0fa3 100644
--- a/test-suite/bugs/bug_4780.v
+++ b/test-suite/bugs/bug_4780.v
@@ -22,8 +22,8 @@ Notation "( x ; y )" := (existT _ x y) : fibration_scope.
 Open Scope fibration_scope.
 Notation pr1 := projT1.
 Notation pr2 := projT2.
-Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
-Notation "x .2" := (projT2 x) (at level 3) : fibration_scope.
+Notation "x .1" := (projT1 x) : fibration_scope.
+Notation "x .2" := (projT2 x) : fibration_scope.
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
 Arguments idpath {A a} , [A] a.
 Arguments paths_rect [A] a P f y p : rename.
diff --git a/test-suite/bugs/bug_7059.v b/test-suite/bugs/bug_7059.v
index e2450cac976c..821e524ec4c7 100644
--- a/test-suite/bugs/bug_7059.v
+++ b/test-suite/bugs/bug_7059.v
@@ -14,8 +14,8 @@ Notation "( x ; y )" := (existT _ x y) : core_scope.
 Notation "( x ; y ; z )" := (x ; (y ; z)) : core_scope.
 Notation pr1 := (@projT1 _ _).
 Notation pr2 := (@projT2 _ _).
-Notation "x .1" := (@projT1 _ _ x) (at level 3, format "x '.1'") : core_scope.
-Notation "x .2" := (@projT2 _ _ x) (at level 3, format "x '.2'") : core_scope.
+Notation "x .1" := (@projT1 _ _ x) : core_scope.
+Notation "x .2" := (@projT2 _ _ x) : core_scope.
 Notation "'exists' x .. y , P"
   := (sigT (fun x => .. (sigT (fun y => P)) ..))
        (at level 200, x binder, y binder, right associativity) : type_scope.
diff --git a/test-suite/output/PrintGrammar.out b/test-suite/output/PrintGrammar.out
index d57aec04c120..3856dcd4e148 100644
--- a/test-suite/output/PrintGrammar.out
+++ b/test-suite/output/PrintGrammar.out
@@ -97,7 +97,9 @@ Entry term is
 | "8" LEFTA
   [  ]
 | "1" LEFTA
-  [ SELF; ".("; "@"; global; univ_annot; LIST0 (term LEVEL "9"); ")"
+  [ SELF; ".2"
+  | SELF; ".1"
+  | SELF; ".("; "@"; global; univ_annot; LIST0 (term LEVEL "9"); ")"
   | SELF; ".("; global; univ_annot; LIST0 arg; ")"
   | SELF; "%"; IDENT
   | SELF; "%_"; IDENT ]
diff --git a/test-suite/output/PrintKeywords.out b/test-suite/output/PrintKeywords.out
index 8ee7a98b5bd5..f25f491e162f 100644
--- a/test-suite/output/PrintKeywords.out
+++ b/test-suite/output/PrintKeywords.out
@@ -20,6 +20,8 @@
 .(
 ..
 ...
+.1
+.2
 /
 /\
 :
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 4807413c680a..e31212453a3e 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -99,8 +99,8 @@ Module NTabareau.
 
 Set Typeclasses Dependency Order.
 Unset Typeclasses Iterative Deepening.
-Notation "x .1" := (projT1 x) (at level 3).
-Notation "x .2" := (projT2 x) (at level 3).
+Notation "x .1" := (projT1 x).
+Notation "x .2" := (projT2 x).
 
 Parameter myType: Type. 
 
@@ -141,8 +141,8 @@ Module NTabareauClasses.
 
 Set Typeclasses Dependency Order.
 Unset Typeclasses Iterative Deepening.
-Notation "x .1" := (projT1 x) (at level 3).
-Notation "x .2" := (projT2 x) (at level 3).
+Notation "x .1" := (projT1 x).
+Notation "x .2" := (projT2 x).
 
 Parameter myType: Type. 
 Existing Class myType.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index ef7c164bbc35..b3b203b9533c 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -114,6 +114,11 @@ Notation "'if' c 'is' p 'then' u 'else' v" :=
 
 End IfNotations.
 
+(** Notations for first and second projections *)
+
+Reserved Notation "p .1" (at level 1, left associativity, format "p .1").
+Reserved Notation "p .2" (at level 1, left associativity, format "p .2").
+
 (** Scopes *)
 
 Declare Scope core_scope.
diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v
index 6c8261741aa3..005830383445 100644
--- a/theories/ssr/ssrfun.v
+++ b/theories/ssr/ssrfun.v
@@ -225,8 +225,6 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 (** Parsing / printing declarations. *)
-Reserved Notation "p .1" (at level 2, left associativity, format "p .1").
-Reserved Notation "p .2" (at level 2, left associativity, format "p .2").
 Reserved Notation "f ^~ y" (at level 10, y at level 8, no associativity,
   format "f ^~  y").
 Reserved Notation "@^~ x" (at level 10, x at level 8, no associativity,

From 39131994a85de4cd2edcb27bbed8428c8301cae9 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Sat, 14 Oct 2023 21:43:58 +0200
Subject: [PATCH 2/3] [ssr] Stop relying on camlp5 recovery mechanism

for "do [tac] => intro" and "tac; [tac|..|tac] => intro"
---
 plugins/ssr/ssrparser.mlg | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 14a0785c2dbd..8c1b88b45400 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1709,7 +1709,10 @@ let tclintros_expr ?loc tac ipats =
 
 GRAMMAR EXTEND Gram
   GLOBAL: ltac_expr;
-  ltac_expr: LEVEL "1" [
+  ltac_expr: LEVEL "3" [
+    [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
+    ] ];
+  ltac_expr: LEVEL "4" [
     [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
     ] ];
 END

From fe63e2331890ca5ac581d6984007be8d10a23260 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 3 Nov 2023 15:21:11 +0100
Subject: [PATCH 3/3] Add overlays

---
 dev/ci/user-overlays/18224-proux01-ssr_17876.sh | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 dev/ci/user-overlays/18224-proux01-ssr_17876.sh

diff --git a/dev/ci/user-overlays/18224-proux01-ssr_17876.sh b/dev/ci/user-overlays/18224-proux01-ssr_17876.sh
new file mode 100644
index 000000000000..8493333c29e5
--- /dev/null
+++ b/dev/ci/user-overlays/18224-proux01-ssr_17876.sh
@@ -0,0 +1,3 @@
+overlay equations https://github.com/proux01/Coq-Equations coq_18224 18224
+overlay metacoq https://github.com/proux01/metacoq coq_18224 18224
+overlay elpi https://github.com/proux01/coq-elpi coq_18224 18224