Merge PR #18224: [ssr] Stop relying on camlp5 recovery mechanism

Reviewed-by: gares Co-authored-by: gares <gares@users.noreply.github.com>
coq · Mar 14, 2024 · 0f0f505 · 0f0f505
2 parents 3925dc3 + fe63e23
commit 0f0f505
Show file tree

Hide file tree

Showing 27 changed files with 59 additions and 46 deletions.
diff --git a/dev/ci/user-overlays/18224-proux01-ssr_17876.sh 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
diff --git 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

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -20,6 +20,8 @@
 .(
 ..
 ...
+.1
+.2
 /
 /\
 :

diff --git 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
@@ -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
@@ -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,