From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- 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/vm_evars.v') diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v new file mode 100644 index 00000000..2c8b099e --- /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