From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 test-suite/success/evars.v | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

(limited to 'test-suite/success/evars.v')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4e2bf451..0f9fb745 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -23,7 +23,7 @@ Definition f1 frm0 a1 : B := f frm0 a1.
 (* Checks that solvable ? in the type part of the definition are harmless *)
 Definition f2 frm0 a1 : B := f frm0 a1.
 
-(* Checks that sorts that are evars are handled correctly (bug 705) *)
+(* Checks that sorts that are evars are handled correctly (BZ#705) *)
 Require Import List.
 
 Fixpoint build (nl : list nat) :
@@ -58,11 +58,11 @@ Check
     (forall y n : nat, {q : nat | y = q * n}) ->
     forall n : nat, {q : nat | x = q * n}).
 
-(* Check instantiation of nested evars (bug #1089) *)
+(* Check instantiation of nested evars (BZ#1089) *)
 
 Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
 
-(* This used to fail with anomaly (Pp.str "evar was not declared") in V8.0pl3 *)
+(* This used to fail with anomaly (Pp.str "evar was not declared.") in V8.0pl3 *)
 
 Theorem contradiction : forall p, ~ p -> p -> False.
 Proof. trivial. Qed.
@@ -188,7 +188,7 @@ Abort.
 
 End Additions_while.
 
-(* Two examples from G. Melquiond (bugs #1878 and #1884) *)
+(* Two examples from G. Melquiond (BZ#1878 and BZ#1884) *)
 
 Parameter F1 G1 : nat -> Prop.
 Goal forall x : nat, F1 x -> G1 x.
@@ -207,7 +207,7 @@ Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) :=
   | (existT _ k v)::l' => (existT _ k v):: (filter A l')
   end.
 
-(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by
+(* BZ#2000: used to raise Out of memory in 8.2 while it should fail by
    lack of information on the conclusion of the type of j *)
 
 Goal True.
@@ -381,7 +381,7 @@ Section evar_evar_occur.
   Check match g _ with conj a b => f _ a b end.
 End evar_evar_occur.
 
-(* Eta expansion (bug #2936) *)
+(* Eta expansion (BZ#2936) *)
 Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }.
 Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri {
   tri0 : forall a b c, R a b -> S a c -> T b c
@@ -414,4 +414,15 @@ Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2.
 Import EqNotations.
 Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a.
 
+(* Check that pre-existing evars are not counted as newly undefined in "set" *)
+(* Reported by Théo *)
 
+Goal exists n : nat, n = n -> True.
+eexists.
+set (H := _ = _).
+Abort.
+
+(* Check interpretation of default evar instance in pretyping *)
+(* (reported as bug #7356) *)
+
+Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z).
-- 
cgit v1.2.3