7 files changed, 138 insertions, 117 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f064dfe763..97fa8e2542 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -80,3 +80,49 @@ fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
 The constructor D (in type J) expects 3 arguments.
+lem1 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+lem2 = 
+fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
+     : forall k : bool, k = k
+
+Argument scope is [bool_scope]
+lem3 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+1 subgoal
+  
+  x : nat
+  n, n0 := match x + 0 with
+           | 0 => 0
+           | S _ => 0
+           end : nat
+  e,
+  e0 := match x + 0 as y return (y = y) with
+        | 0 => eq_refl
+        | S n => eq_refl
+        end : x + 0 = x + 0
+  n1, n2 := match x with
+            | 0 => 0
+            | S _ => 0
+            end : nat
+  e1, e2 := match x return (x = x) with
+            | 0 => eq_refl
+            | S n => eq_refl
+            end : x = x
+  ============================
+  x + 0 = 0
+1 subgoal
+  
+  p : nat
+  a,
+  a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : eq_refl = eq_refl /\ p = p
+  a1,
+  a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : p = p /\ p = p
+  ============================
+  eq_refl = eq_refl
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 6a4fd007df..17fee3303d 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -121,3 +121,66 @@ Check fun x => let '(D n m p q) := x in n+m+p+q.
 (* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
 
 Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
+
+(* Test use of idents bound to ltac names in a "match" *)
+
+Lemma lem1 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end).
+Qed.
+Print lem1.
+
+Lemma lem2 : forall k, k=k :> bool.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k => if k as x return x = x then eq_refl else eq_refl).
+Qed.
+Print lem2.
+
+Lemma lem3 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl).
+Qed.
+Print lem3.
+
+Lemma lem4 x : x+0=0.
+match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+Show.
+
+Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
+let y := fresh "n" in (* Checking that y is hidden *)
+  let z := fresh "e" in (* Checking that z is hidden *)
+  match goal with
+  |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let p := fresh "p" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+Show.
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index 6c514b16ee..1ecd9771eb 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -1,5 +1,7 @@
 (** Extraction : tests of optimizations of pattern matching *)
 
+Require Coq.extraction.Extraction.
+
 (** First, a few basic tests *)
 
 Definition test1 b :=
diff --git a/test-suite/output/Int31Syntax.out b/test-suite/output/Int31Syntax.out
new file mode 100644
index 0000000000..4e8796c14b
--- /dev/null
+++ b/test-suite/output/Int31Syntax.out
@@ -0,0 +1,14 @@
+I31
+     : digits31 int31
+2
+     : int31
+660865024
+     : int31
+2 + 2
+     : int31
+2 + 2
+     : int31
+     = 4
+     : int31
+     = 710436486
+     : int31
diff --git a/test-suite/output/Int31Syntax.v b/test-suite/output/Int31Syntax.v
new file mode 100644
index 0000000000..83be3b976b
--- /dev/null
+++ b/test-suite/output/Int31Syntax.v
@@ -0,0 +1,13 @@
+Require Import Int31 Cyclic31.
+
+Open Scope int31_scope.
+Check I31. (* Would be nice to have I31 : digits->digits->...->int31
+              For the moment, I31 : digits31 int31, which is better
+	      than (fix nfun .....) size int31 *)
+Check 2.
+Check 1000000000000000000. (* = 660865024, after modulo 2^31 *)
+Check (add31 2 2).
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
+Close Scope int31_scope.
diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out
deleted file mode 100644
index b2677b6ad1..0000000000
--- a/test-suite/output/NumbersSyntax.out
+++ /dev/null
@@ -1,67 +0,0 @@
-I31
-     : digits31 int31
-2
-     : int31
-660865024
-     : int31
-2 + 2
-     : int31
-2 + 2
-     : int31
-     = 4
-     : int31
-     = 710436486
-     : int31
-2
-     : BigN.t'
-1000000000000000000
-     : BigN.t'
-2 + 2
-     : bigN
-2 + 2
-     : bigN
-     = 4
-     : bigN
-     = 37151199385380486
-     : bigN
-     = 1267650600228229401496703205376
-     : bigN
-2
-     : BigZ.t_
--1000000000000000000
-     : BigZ.t_
-2 + 2
-     : BigZ.t_
-2 + 2
-     : BigZ.t_
-     = 4
-     : BigZ.t_
-     = 37151199385380486
-     : BigZ.t_
-     = 1267650600228229401496703205376
-     : BigZ.t_
-2
-     : BigQ.t_
--1000000000000000000
-     : BigQ.t_
-2 + 2
-     : bigQ
-2 + 2
-     : bigQ
-     = 4
-     : bigQ
-     = 37151199385380486
-     : bigQ
-6562 # 456
-     : BigQ.t_
-     = 3281 # 228
-     : bigQ
-     = -1 # 10000
-     : bigQ
-     = 100
-     : bigQ
-     = 515377520732011331036461129765621272702107522001
-       # 1267650600228229401496703205376
-     : bigQ
-     = 1
-     : bigQ
diff --git a/test-suite/output/NumbersSyntax.v b/test-suite/output/NumbersSyntax.v
deleted file mode 100644
index 4fbf56ab1d..0000000000
--- a/test-suite/output/NumbersSyntax.v
+++ /dev/null
@@ -1,50 +0,0 @@
-
-Require Import BigQ.
-
-Open Scope int31_scope.
-Check I31. (* Would be nice to have I31 : digits->digits->...->int31
-              For the moment, I31 : digits31 int31, which is better
-	      than (fix nfun .....) size int31 *)
-Check 2.
-Check 1000000000000000000. (* = 660865024, after modulo 2^31 *)
-Check (add31 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
-Close Scope int31_scope.
-
-Open Scope bigN_scope.
-Check 2.
-Check 1000000000000000000.
-Check (BigN.add 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
-Eval vm_compute in 2^100.
-Close Scope bigN_scope.
-
-Open Scope bigZ_scope.
-Check 2.
-Check -1000000000000000000.
-Check (BigZ.add 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
-Eval vm_compute in (-2)^100.
-Close Scope bigZ_scope.
-
-Open Scope bigQ_scope.
-Check 2.
-Check -1000000000000000000.
-Check (BigQ.add 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
-(* fractions *)
-Check (6562 # 456). (* Nota: # is BigQ.Qq i.e. base fractions *)
-Eval vm_compute in (BigQ.red (6562 # 456)).
-Eval vm_compute in (1/-10000).
-Eval vm_compute in (BigQ.red (1/(1/100))). (* back to integers... *)
-Eval vm_compute in ((2/3)^(-100)).
-Eval vm_compute in BigQ.red ((2/3)^(-1000) * (2/3)^(1000)).
-Close Scope bigQ_scope.