Merge PR #11240: Add rew dependent Notations

Reviewed-by: herbelin
Ack-by: jfehrle

2 files changed, 128 insertions, 2 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 94b86fc222..b870fa6f6f 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -137,3 +137,71 @@ end = p
      : forall x : nat, x = x -> Prop
 bar  0
      : nat
+let k := rew [P] p in v in k
+     : P y
+let k := rew [P] p in v in k
+     : P y
+let k := rew <- [P] p in v' in k
+     : P x
+let k := rew [P] p in v in k
+     : P y
+let k := rew [P] p in v in k
+     : P y
+let k := rew <- [P] p in v' in k
+     : P x
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+     : P x
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+     : P x
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+     : P y p
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+     : P y p
+let k := rew dependent <- [fun y0 p => id (P' y0 p)] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+     : P y p
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+     : P y p
+let k := rew dependent <- [fun y0 p0 => id (P' y0 p0)] p in v' in k
+     : P' x (eq_sym p)
+rew dependent [P] p in v
+     : P y p
+rew dependent <- [P'] p in v'
+     : P' x (eq_sym p)
+rew dependent [fun a x => id (P a x)] p in v
+     : id (P y p)
+rew dependent <- [fun a p' => id (P' a p')] p in v'
+     : id (P' x (eq_sym p))
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adab324cf0..7d2f1e9ba8 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -251,11 +251,11 @@ Notation NONE := None.
 Check (fun x => match x with SOME x => x | NONE => 0 end).
 
 Notation NONE2 := (@None _).
-Notation SOME2 := (@Some _).     
+Notation SOME2 := (@Some _).
 Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
 
 Notation NONE3 := @None.
-Notation SOME3 := @Some.     
+Notation SOME3 := @Some.
 Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end).
 
 Notation "a :'" := (cons a) (at level 12).
@@ -300,3 +300,61 @@ Definition bar (a b : nat) := plus a b.
 Notation "" := A (format "", only printing).
 Check (bar A 0).
 End M.
+
+(* Check eq notations *)
+Module EqNotationsCheck.
+  Import EqNotations.
+  Section nd.
+    Context (A : Type) (x : A) (P : A -> Type)
+            (y : A) (p : x = y) (v : P x) (v' : P y).
+
+    Check let k : P y := rew p in v in k.
+    Check let k : P y := rew -> p in v in k.
+    Check let k : P x := rew <- p in v' in k.
+    Check let k : P y := rew [P] p in v in k.
+    Check let k : P y := rew -> [P] p in v in k.
+    Check let k : P x := rew <- [P] p in v' in k.
+    Check let k : P y := rew [fun y => P y] p in v in k.
+    Check let k : P y := rew -> [fun y => P y] p in v in k.
+    Check let k : P x := rew <- [fun y => P y] p in v' in k.
+    Check let k : P y := rew [fun (y : A) => P y] p in v in k.
+    Check let k : P y := rew -> [fun (y : A) => P y] p in v in k.
+    Check let k : P x := rew <- [fun (y : A) => P y] p in v' in k.
+  End nd.
+  Section dep.
+    Context (A : Type) (x : A) (P : forall y, x = y -> Type)
+            (y : A) (p : x = y) (P' : forall x, y = x -> Type)
+            (v : P x eq_refl) (v' : P' y eq_refl).
+
+    Check let k : P y p := rew dependent p in v in k.
+    Check let k : P y p := rew dependent -> p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- p in v' in k.
+    Check let k : P y p := rew dependent [P] p in v in k.
+    Check let k : P y p := rew dependent -> [P] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [P'] p in v' in k.
+    Check let k : P y p := rew dependent [fun y p => P y p] p in v in k.
+    Check let k : P y p := rew dependent -> [fun y p => P y p] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => P' y p] p in v' in k.
+    Check let k : P y p := rew dependent [fun y p => id (P y p)] p in v in k.
+    Check let k : P y p := rew dependent -> [fun y p => id (P y p)] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => id (P' y p)] p in v' in k.
+    Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+    Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => P' x p)] p in v' in k.
+    Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+    Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => id (P' x p))] p in v' in k.
+    Check match p as x in _ = a return P a x with
+          | eq_refl => v
+          end.
+    Check match eq_sym p as p' in _ = a return P' a p' with
+          | eq_refl => v'
+          end.
+    Check match p as x in _ = a return id (P a x) with
+          | eq_refl => v
+          end.
+    Check match eq_sym p as p' in _ = a return id (P' a p') with
+          | eq_refl => v'
+          end.
+  End dep.
+End EqNotationsCheck.