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/success') diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v new file mode 100644 index 000000000..2c8b099ef --- /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