From f0bd95e051480e15348e9d30e2df5d3577a9ffb3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Jul 2017 18:58:25 +0200
Subject: Adding a test file for evar handling in the VM.

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

(limited to 'test-suite')

diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v
new file mode 100644
index 0000000000..2c8b099ef0
--- /dev/null
+++ b/test-suite/success/vm_evars.v
@@ -0,0 +1,23 @@
+Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) :=
+match n with
+| 0 => x
+| S n => iter n f (f x)
+end.
+
+Goal nat -> True.
+Proof.
+intros n.
+evar (f : nat -> nat).
+cut (iter 10 f 0 = 0).
+vm_compute.
+intros; constructor.
+instantiate (f := (fun x => x)).
+reflexivity.
+Qed.
+
+Goal exists x, x = 5 + 5.
+Proof.
+  eexists.
+  vm_compute.
+  reflexivity.
+Qed.
-- 
cgit v1.2.3


From 0e79cec728dd4cfc3596a39b5d8bede663fea73c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Jul 2017 22:42:43 +0200
Subject: Removing test for bug #2850.

This test was actually checking that evar-containing terms were making the
VM fail. Obviously this is not the case anymore, so the test is now invalid.
---
 test-suite/bugs/closed/2850.v | 2 --
 1 file changed, 2 deletions(-)
 delete mode 100644 test-suite/bugs/closed/2850.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v
deleted file mode 100644
index 64a93aeb00..0000000000
--- a/test-suite/bugs/closed/2850.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Definition id {A} (x : A) := x.
-Fail Compute id.
-- 
cgit v1.2.3