Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

4 files changed, 41 insertions, 2 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index beba8df9..66307236 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -127,3 +127,12 @@ Identifier 'foo' now a keyword
      : nat
 fun _ : nat => 9
      : nat -> nat
+Identifier 'ONE' now a keyword
+fun (x : nat) (p : x = x) => match p with
+                             | ONE => ONE
+                             end = p
+     : forall x : nat, x = x -> Prop
+fun (x : nat) (p : x = x) => match p with
+                             | 1 => 1
+                             end = p
+     : forall x : nat, x = x -> Prop
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 52f499ab..612b5325 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -262,3 +262,16 @@ Notation "'foo' n" := (S n) (at level 50): nat_scope.
 
 Check (foo 9).
 Check (fun _ : nat => 9).
+
+(* Checking parsing and printing of numerical and non-numerical notations for eq_refl *)
+
+(* This notation was not correctly printed until Pierre B.'s
+   improvements to the interpretation of patterns *)
+
+Notation "'ONE'" := eq_refl.
+Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p.
+
+(* This one used to failed at parsing until now *)
+
+Notation "1" := eq_refl.
+Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index f445ca8e..c9a3c08e 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1865,3 +1865,9 @@ Type (fun n => match n with
                | Z0 => true
                | _ => false
                end).
+
+(* Check that types with unknown sort, as A below, are not fatal to
+   the pattern-matching compilation *)
+
+Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
+  match p with eq_refl => u end.
diff --git a/test-suite/success/set.v b/test-suite/success/set.v
index 23019275..8116e897 100644
--- a/test-suite/success/set.v
+++ b/test-suite/success/set.v
@@ -1,8 +1,19 @@
+(* This used to fail in 8.0pl1 *)
+
 Goal forall n, n+n=0->0=n+n.
 intros.
-
-(* This used to fail in 8.0pl1 *)
 set n in * |-.
+Abort.
+
+(* This works from 8.4pl1, since merging of different instances of the
+   same metavariable in a pattern is done modulo conversion *)
+
+Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1").
+
+Goal forall (f:forall n, n=0 -> Prop) n (H:(n+n).+1=0), f (n.+1+n) H.
+intros.
+set (f _ _).
+Abort.