From 3074967fd01acc5987eb2ea648fcfe32aeca1749 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 12:27:53 +0200
Subject: Few tests for e-variants of assert, set, remember.

---
 test-suite/success/forward.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/success/forward.v

(limited to 'test-suite')

diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
new file mode 100644
index 0000000000..0ed5b524f3
--- /dev/null
+++ b/test-suite/success/forward.v
@@ -0,0 +1,18 @@
+(* Testing forward reasoning *)
+
+Goal 0=0.
+Fail assert (_ = _).
+eassert (_ = _)by reflexivity.
+eassumption.
+Qed.
+
+Goal 0=0.
+Fail set (S ?[nl]).
+eset (S ?[n]).
+remember (S ?n) as x.
+instantiate (n:=0).
+Fail remember (S (S _)).
+eremember (S (S ?[x])).
+instantiate (x:=0).
+reflexivity.
+Qed.
-- 
cgit v1.2.3


From bbde815f8108f4641f5411d03f7a88096cc2221b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 24 May 2017 21:55:21 +0200
Subject: Support for using type information to infer more precise evar
 sources.

This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).

Incidentally updating output of Show output test (evar numbers shifted).
---
 test-suite/.csdp.cache          | Bin 89077 -> 89077 bytes
 test-suite/output/Show.out      |   6 +++---
 test-suite/output/inference.out |  10 +++++-----
 test-suite/output/inference.v   |   2 +-
 test-suite/output/names.out     |   6 ++++++
 test-suite/output/names.v       |   4 ++++
 test-suite/success/Abstract.v   |   1 -
 7 files changed, 19 insertions(+), 10 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b99d80e95f..ba85286dd3 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index bf1bf2809d..8acfed5d00 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,12 +1,12 @@
-3 subgoals (ID 29)
+3 subgoals (ID 31)
   
   H : 0 = 0
   ============================
   1 = 1
 
-subgoal 2 (ID 33) is:
+subgoal 2 (ID 35) is:
  1 = S (S m')
-subgoal 3 (ID 20) is:
+subgoal 3 (ID 22) is:
  S (S n') = S m
 
 (dependent evars: (printing disabled) )
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c70467912f..d28ee42761 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x : T n := A n in ?t ?y : T n
+fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where
-?t : [n : nat  x := A n : T n |- ?T -> T n] 
-?y : [n : nat  x := A n : T n |- ?T] 
-fun n : nat => ?t ?y : T n
+?t : [n : nat  y := A n : T n |- ?T -> T n] 
+?x : [n : nat  y := A n : T n |- ?T] 
+fun n : nat => ?t ?x : T n
      : forall n : nat, T n
 where
 ?t : [n : nat |- ?T -> T n] 
-?y : [n : nat |- ?T] 
+?x : [n : nat |- ?T] 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 1825db1676..f761a4dc5a 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 (* Note: exact numbers of evars are not important... *)
 
 Inductive T (n:nat) : Type := A : T n.
-Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 9471b892dd..48be63a46a 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -3,3 +3,9 @@ In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
 while it is expected to have type "{x : nat | x = y}".
+1 focused subgoal
+(shelved: 1)
+  
+  H : ?n <= 3 -> 3 <= ?n -> ?n = 3
+  ============================
+  True
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
index b3b5071a03..f1efd0df2a 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -3,3 +3,7 @@
 
 Parameter a : forall x, {y:nat|x=y}.
 Fail Definition b y : {x:nat|x=y} := a y.
+
+Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
+intro H; epose proof (H _ 3) as H.
+Show.
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index ffd50f6efd..69dc9aca78 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,3 @@
-
 (* Cf coqbugs #546 *)
 
 Require Import Omega.
-- 
cgit v1.2.3